突發消息：消費者版本的亞里士多德擊敗了普特南，解決並正式驗證了 @leanprover 中的 10/12 題目。 恭喜業餘數學家 @namrata_anand2，使用消費者級版本的亞里士多德和問題的早期公開版本。看起來亞里士多德把它們當早餐吃了，完全自主地解決了 10/12 題目。 我們目前正在深入研究這些文件，稍後會分享更多細節，但現在有兩件有用的事情需要指出： ▪️這似乎是首次公開發布的 2025 年普特南問題的完全形式化解決方案。 ▪️這些都使用了最近發布的自然語言介面，亞里士多德以自然語言接收問題，然後自動將其形式化為 Lean4 陳述，並完全自主地完成證明，沒有任何人參與。過去，我們專注於亞里士多德的尖端定理證明能力，但它在自動形式化方面也變得相當有能力。 我們正進入 AI 和數學的新曙光。慢慢來……然後一下子！