AI三周解决11个LeanEval难题

研究员Vasily Ilin在X上宣布，过去三周内利用AI解决了11个此前未解的LeanEval问题，包括Green-Tao定理、Morley范畴定理等大型研究级形式化难题。这一进展展示了AI在数学形式化领域的加速能力，有观点预测到2027年95%的新论文可在一天内完成形式化。

2026-08-14 ~ 2026-08-14 · 2 条相关

• AI 数学形式化加速：3周解决11个难题，2027年95%新论文可一天形式化 — RexDouglass · 2026-08-14
• 三周解决11个LeanEval难题，含Green-Tao定理 — TacoCohen · 2026-08-14