问数学部分尚未正式化/伊莎贝尔愿望表

EN

就在我头顶上：

• 有Freek Wiedijk关于100个有趣定理的列表和不同的人一直致力于形式化的定理从名单(包括我)，但这主要是为了好玩。
• 也有正在进行的努力(主要由Larry )来移植HOL的结果(主要是复杂的分析，但也包括拓扑和几何学)。
• Innsbruck的人一直在从事与多项式相关的大量工作(例如，这里)；我认为，主要是因为他们需要它作为重写系统中的终止证明。
• 有一个用于形式化自动机和模型检查的CAVA项目。

没有真正的“大伊莎贝尔委员会”来选择一个每个人在未来几年都应该关注的数学领域，但是有一些项目和小组或多或少是独立于彼此的。

对于常微分方程，费边·伊姆勒在这方面做了大量的工作。他目前正在研究洛伦兹吸引器确实是混乱的证据，这需要相当多复杂的与代码相关的材料和算法。

你是正确的，ε-δ-论点是一个绝对可怕的形式，这就是为什么我们不这样做。伊莎贝尔中的限制和导数是关于过滤器(例如这里)的形式化的，这是表达这种推理的一种非常优雅的方式。

至于那些很好的东西，据我所知，现在没有人在研究：

• 在Freek Wiedijk的名单上还没有在伊莎贝尔做过的事
• 如果伊莎贝尔有更多的抽象代数，那就太好了。(我们没有那么多代数的原因之一可能是Coq人已经有了很多代数，使用依赖类型也可能更好)
• 没有太多的数论
• 用流形和向量分析(散度、弯曲、曲面积分、等高线积分)的理论是很好的。
• 我非常喜欢分析组合学，但我担心我们所拥有的那种渐近分析的自动化目前还不够。