定理证明器

Harmonic公司开发的AI系统Aristotle近日在解决Erdős第728号数论难题上取得进展。系统将英文非正式证明自动翻译为Lean形式化代码，并由Lean微内核逐步校验，证明一旦通过即可保证逻辑无误，降低生成式AI“幻觉”。项目早期需数学家Terence Tao协助澄清定义，随后AI能自查漏洞并修复论证，已向Mathlib提交多项贡献。该模式在代数、数论等基础完备领域有望加速科研迭代，但在拓扑等缺少形式化定义的方向仍受限。