我很好奇当前数学形式化的“状态”是什么，是否可能存在某种趋势来证明某个数学领域的结果，或者是否存在协调一致的努力来证明某些事情？
浏览形式证明文件，在我看来，情况并非如此，因为不同的人正在努力将数学的各个部分形式化，但不是以协调的方式(并不是一定需要，我只是好奇)。
是否有一些数学部分或主要定理尚未形式化并且目前在愿望 list 中排名靠前？
特别是，在(普通)微分方程领域似乎没有做太多的工作 - 但我(非常天真的)印象是，形式化这些结果非常困难，因为经常出现的那种 epsilon-delta 推理所遇到的问题并不容易形式化，特别是因为数学本身通常在这个领域中以一种更方便的方式完成(与数学的更多代数部分形成鲜明对比，这些部分通常更精确地编写完成并且 - 我是猜测——形式化起来不那么繁琐)。这种印象正确吗？
最佳答案
就在我的头顶上:
- 有Freek Wiedijk's list of 100 interesting theorems许多人一直在致力于将该列表中的定理形式化(包括我)，但这主要是为了好玩。
- 我们还在努力(主要由 Larry Paulson)移植 HOL Light 的结果(主要是复杂分析，但也包括拓扑和几何)。
- 来自因斯布鲁克的人们一直致力于大量与多项式相关的研究(参见 here )；我认为主要是因为他们需要它来作为重写系统的终止证明
- 有 CAVA project适用于形式化自动机和模型检查
实际上并没有一个“大伊莎贝尔委员会”来选择一个每个人在未来几年都应该关注的数学领域，但有一些项目和团体或多或少彼此独立地完成这一任务。
对于常微分方程，Fabian Immler在过去的几年里，我们在这方面做了很多令人印象深刻的工作。他目前正在证明洛伦兹吸引子确实是混沌的，这需要大量复杂的 ODE 相关 Material 和算法。
你是对的，ε-δ-论证对于形式化来说绝对是可怕的，这就是我们不这样做的原因。 Isabelle 中的限制和导数是针对过滤器进行形式化的(例如 here )，这是表达此类推理的一种非常优雅的方式。
至于那些本来就很好的事情，据我所知，目前没有人在做:
- 几乎所有 Freek Wiedijk list 上尚未在伊莎贝尔完成的事情
- 如果伊莎贝尔能有更多抽象代数就好了。 (我们没有那么多代数的原因之一可能是因为 Coq 人已经有很多代数了；用依赖类型来做这件事可能会更好)
- 没有太多的数论
- 流形和矢量分析理论(散度、旋度、表面积分、轮廓积分)会很好
- 我是分析组合学的忠实粉丝，但我担心目前我们所需要的渐近分析自动化程度还不够。
关于isabelle - 部分数学尚未形式化/伊莎贝尔愿望 list ，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/42346842/