LeanMarathon

AI 系统 LeanMarathon 助力复杂数学研究的形式化

研究人员开发了 LeanMarathon，这是一个新的多代理系统，旨在提高 AI 在形式化复杂数学研究方面的可靠性。该系统使用不断演变的蓝图来管理证明骨架、自然语言图和依赖关系，从而实现更强大和并行化的形式化过程。LeanMarathon 成功形式化了近期两篇研究论文中的所有定理，包括与 Erdős 问题相关的定理，证明了其在处理长时程数学发展而无错误的能力。