世界上最难的本科生数学竞赛——普特南数学竞赛，于昨天下午4点（太平洋时间）结束。 下午 3:58，AxiomProver @axiommathai 自主解决了 12 道 Putnam2025 题目中的 8 道（使用 Lean 语言），Lean 是一种 100% 可验证的语言。 去年，我们的得分在约 4000 所学校中排名第 4，并能获得 Putnam 奖学金（近年来排名前 10）。
威廉·洛厄尔·普特南考试是世界上最负盛名的大学入学考试。中位数分数通常为0。 Axiom是一家位于帕洛阿尔托的初创公司，成立至今已有4个月。我们正在构建推理的起点：一个人工智能数学家。 Lean 是一种 100% 机器可验证的语言。
这是我们的第一步。 四个月前，我们只有从旧货市场淘来的露营椅和塑料桌子。白板就是贴在墙上的便利贴。大家对我们的第一张沙发都欣喜若狂。 现在，我们已在大西洋彼岸扎根。 一支拥有超强数学和工程学实力的团队，正在汇聚一堂！
我们 AxiomProver 系统背后的团队热爱数学、编程语言和人工智能——这三大支柱。 他们争论形式化是否自然。当编译器技术使证明得以通过时，他们会感到兴奋。 这项工作技术性很强，但同时也充满了人文关怀。
我们站在巨人的肩膀上——@leanprover、Mathlib 社区以及学术界和工业界的研究人员。 谢谢，我们正在开发相关工具，以便在未来的版本中更好地服务社区。 我们向普特南杯的参赛者致敬，并将很快庆祝你们取得的成就。
@axiommathai 会非常感谢您的转发！