formalized_mathematics

理解 formalized mathematics

formalized有形式化正式化的意思，与自然语言相对

理论

dependent_type_theory homotopy_type_theory 构造主义数学

有一定坚实的基础是必要的, 但基础并不等于全部

你如果实地去采访数学家，跟他们聊聊这种不能证明又不能证伪的，所谓独立性的现象，如果他们还有兴趣跟你继续下去这段对话，你基本上就会发现，那些平时对什么公理体系啊可证性啊集合论啊不感兴趣的人，基本上在这上面就是持灵活滑雪主义：哪个态度能让我做出赏心悦目的数学、让我发出令人尊敬的论文，我就选择哪个态度。我甚至不需要统一地保持一个态度，在哪里我就是哪里人。
@如何通俗理解一个数学命题既不能证明又不能证伪？

Set theory is the coroner of math. It pronounces your problem dead.
@Matthew Foreman

语言

LEAN.mathlib

[[Agda]]
[[Public/fu_language]]

AI4math

Robust_Prover

【【重构数学4/4】未来的重构：数学、代码与人工智能-哔哩哔哩】 https://b23.tv/Qe2g2BH
AI
数学的目的：找deep的命题和好的链接方式，探索未知，连接已知
命题：枢纽（lemma，proof等），节点
重构枢纽

不过有个比较Tricky的地方，就是证明最重要的原则是“人类可以理解”，因为实际上有些命题并没有想象那么重要，之前用数值验证已经检验了大家用得到的情况，在探索中发现的一些规律和方法可能才是比较重要的。用这种语言写出来也不是说完全不能理解吧，但可读性会差一些