AxiomMath宣布在Lean中完成Stacks Project的形式化

AxiomMath宣布已对数学参考文献库Stacks Project完成形式化验证。TechCrunch在十一月5日发表的文章中报道，该公司的AI智能体已将其中约7,654页内容转换为约1600万行经计算机验证的代码。据该媒体报道，这一消息于星期三公布。

这项工作基于Lean开展。在这种语言中，证明被重新表述为代码，再由证明助手检查。对于如此庞大的文献库，挑战不止于逐一验证每个定理：定义与结论之间存在相互依赖关系。AxiomMath解释说，必须在整个转换过程中保留这些关系。

该公司将此次形式化工作描述为可重复使用的基础，尤其适用于代数几何。据其团队介绍，此前，希望在这一领域验证新研究成果的研究人员在Lean中可用的基础很少。其智能体在分层组织下并行工作，并拥有一定的自主空间来确定各自的任务。

潜在价值在于积累经过检验的结论，供其他证明使用。AxiomMath还希望将这一方法应用于软件。这一前景仍是愿景：报道中的公告涉及数学形式化，其本身并不能证明智能体能够生成没有缺陷的软件。