形式化数学方面的工作还是比较多的，著名一些的例子有Kepler Conjecture (i.e. The Flyspeck Project) [1], Four Color Theorem [2], Odd Order Theorem [3], Jordan Curve Theorem [4], Godel’s Incompleteness Theorems [5], Prime Number Theorem [6,7] 以及 Central Limit Theorem [8]。 另外Freek Wiedilk 维护的网页Formalizing 100 Theorems ( http://www.cs.ru.nl/~freek/100/ )可以看到一些比较著名的定理在各个定理证明器中被形式化的现状。好处一：因为每一步都需要严格的推理，所以不会出错。
在关注证明正确性的同时，其实还有一个可读性/可解释性的问题。一个关于证明在数学里角色的观点是：
- 一个证明应当说服读者某个命题的正确性（A proof convinces the reader that the statement is correct）。
- 一个证明应当能解释为什么某个命题是正确的 （A proof explains why the statement is correct）。
对于第一点，把证明分解到公理级别的推理步骤，再由程序来检查即可。但是对于第二点，我们往往需要结构化且人类可读的形式化证明，甚至需要超越形式化语言的自然语言来描述证明背后的思想(intuition)。进一步关于这方面的讨论可以看看Herman Geuvers [9] 和 Leslie Lamport [10]的文章。好处二：人类既有成果的电子化，为未来AI启发式证明提供基本的框架与库。
同时我们也要意识到在一个有相当表达力的逻辑下做自动推理是相当困难的。就被AlphaGo/AlphaZero解决的围棋而言，整个游戏是在一阶逻辑下的（如果我没理解错的话），而且游戏本身还还是可判定的（decidable，存在一个算法在有限步骤内判定真值）， 当然计算代价是极其巨大的。广义一阶逻辑下的命题已是是不可判定的，表达力在一阶逻辑之上的高阶逻辑（quantify over predicates and functions)就更难了， 在上面还有能把图灵机嵌在类型系统里的CIC(Coq所用的逻辑)。目前有一些把深度学习应用到自动推理方向到尝试，不过目前效果还比较有限，主流的方法还是传统的resolution/superposition-based prover + SMT solver以及一大堆人工设置的启发策略（heuristics）。
目前在Isabelle证明器下有 Archive of Formal Proofs,这是一个有着超过180万行证明的代码库。在Mizar证明器下有 Mizar Mathematical Library, 其中有着超过52000条被证明的定理。我们相信这些已有的证明能为未来的自动定理证明提供训练数据。
另外，关于 @Yuhang Liu 答主提到的证明中概念抽象的问题，正如 @Qinxiang Cao答主所说，我们在定理证明器中定义概念是有层次（封装）的，高层次的推理一般是不用考虑底层的定义。比如在Isabelle/HOL中的微分是基于Frechet derivative：
![]()
当然这里的bounded_linear, Lim, norm等函数还有各自的形式化定义。但是进行微分相关的推理时，我们几乎已经不用考虑微分的定义，而是直接使用在这个定义基础上证明出的微分的相关性质，例如：
![]()
微分中的链式法则![]()
可导一定连续[1] Hales, Thomas C. "Introduction to the Flyspeck project." Dagstuhl Seminar Proceedings. Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2006.
[2] Gonthier, Georges. "Formal proof–the four-color theorem." Notices of the AMS 55.11 (2008): 1382-1393.
[3] Gonthier, Georges, et al. "A machine-checked proof of the odd order theorem." International Conference on Interactive Theorem Proving. Springer, Berlin, Heidelberg, 2013.
[4] Hales, Thomas C. "The Jordan curve theorem, formally and informally." American Mathematical Monthly 114.10 (2007): 882-894.
[5] Paulson, Lawrence C. "A mechanised proof of Gdel’s incompleteness theorems using Nominal Isabelle." Journal of Automated Reasoning 55.1 (2015): 1-37.
[6] Harrison, John. "Formalizing an analytic proof of the prime number theorem." Journal of Automated Reasoning 43.3 (2009): 243-261.
[7] Avigad, Jeremy, et al. "A formally verified proof of the prime number theorem." ACM Transactions on Computational Logic (TOCL) 9.1 (2007): 2.
[8] Avigad, Jeremy, Johannes Hlzl, and Luke Serafin. "A formally verified proof of the Central Limit Theorem." Journal of Automated Reasoning 59.4 (2017): 389-423.
[9] Geuvers, Herman. "Proof assistants: History, ideas and future." Sadhana 34.1 (2009): 3-25.
[10] Lamport, Leslie. "How to write a 21 st century proof." Journal of fixed point theory and applications 11.1 (2012): 43-63.
|
转播
