🚨 Math Inc的代理人高斯刚刚自动形式化了曲线的黎曼假设证明

🎀 特伦斯·陶与数学公司合作 🎀 作为首位 Veritas Fellow — 以正式化数论中的估计。 在解析数论中，文献中包含大量明确的估计。但这些估计并不立即可互操作。在实践中，结果分为三个层次： 初级估计：这些是基础输入，例如黎曼 ζ 函数的无零区。它们通常依赖于大量计算和仔细的数值优化。 次级估计：许多论文采用初级输入（例如，无零区）并将其转化为可重用的结果，例如在短区间内计数素数。这些成为整个学科中使用的核心构建块。 三级估计：进一步的工作将这些次级构建块应用于前沿数论问题，例如将整数表示为三个素数的和。 困难在于，这些层次并不会随着时间的推移而干净地更新。一篇三级论文可能依赖于当时可用的最佳初级估计。但几年后，改进的计算会细化初级输入，而没有系统地传播到次级和三级链中。因此，“同一定理与更新常数”往往是未知的。 目标是正式化这些层次中的关键论文，然后将其抽象化，使其依赖关系变得明确、可组合和机器可检查。长期愿景是创建一个活的影响网络：当初级估计改进时，每个下游影响都会自动升级。这将把数学文献转变为模块化软件。 数论是一个强有力的测试案例，因为它的估计具有相对清晰的结构，以及一组共享的标准输入和输出。但在许多领域，如 PDE，研究人员不断花费精力进行修改：调整引理和假设，在不兼容的框架之间翻译，“将方钉放入圆孔”。一个可组合的、机器验证的影响网络直接针对这种摩擦。 同样的基础设施有望扩展到其他领域，并使当前难以协调的众包大规模项目成为可能。一个经典的例子是有限简单群的分类：这是一个跨越许多贡献者的数十年努力，必然涉及到记账、整合和完整性信心的复杂性。 借助现代工具，我们设想处理可比范围的重大挑战：许多贡献者处理不同的案例，自动化系统将各个部分粘合在一起。该领域成为一个实时进度仪表板，记录已证明的内容、剩余内容，以及每个组件所需的确切依赖关系。 这为以更快的节奏和更具吸引力的方式进行数学开辟了可能性。 观看陶的概述视频：