Peter Woit

Axiom Math 使用 AI 代理对庞大的数学库进行形式化验证

估值 16 亿美元的初创公司 Axiom Math 正在开发人工智能代理，以确保数学严谨性并防止未经验证的人工智能生成证明的扩散。该公司已对 Stacks Project 进行了形式化验证，这是一个庞大的数学知识集合，使用 Lean 编程语言将其约 7,654 页的内容翻译成 1600 万行计算机检查的代码。此举旨在为人工智能代理在软件开发和科学研究中提供可靠的基础，解决了形式化数学中的一个重大空白，尤其是在代数几何领域。