AI辅助完成11个正方形最优堆叠证明

一项AI辅助证明给出了11个正方形最优堆叠的完整最优性证明，所有7920个本地Lean模块通过验证且最终审计无遗漏，几何与检查器可靠性仍采用常规Lean证明。

• HN讨论：数学家为何抛弃OpenAI2026-10-17
• Thomas Hales谈Lean定理证明器的可靠性与AI2026-10-10
• Bend：用证明阻断AI错误的编程语言2026-09-17
• OpenAI 分享 AI 生成的 Navier–Stokes 解与 Lean 形式化证明2026-09-09