突发消息：消费者版本的亚里士多德击败了普特南，解决并正式验证了 @leanprover 中的 10/12 个问题。 祝贺业余数学家 @namrata_anand2，她使用了消费者级别的亚里士多德和问题的早期公开版本。看起来亚里士多德轻松解决了这些问题，完全自主地解决了 10/12 个。 我们目前正在深入研究这些文件，稍后会分享更多细节，但现在有两件有用的事情需要指出： ▪️这些似乎是首次公开发布的 2025 年普特南问题的完全形式化解决方案。 ▪️这些都使用了最近发布的自然语言接口，亚里士多德以自然语言输入问题，然后将其自动形式化为 Lean4 语句，最后完全自主地完成了证明，没有人参与。在过去，我们专注于亚里士多德的最先进的定理证明能力，但它在自动形式化方面也变得相当强大。 我们正迈入人工智能与数学的新曙光。慢慢来……然后一下子就来了！