Lean 4 真的是一款定理证明器
该比赛已结束，您无法在比赛模式下递交该题目。您可以点击“在题库中打开”以普通模式查看和递交本题。
题目背景
2026 年 9 月 4 日，Anthropic 宣布人工智能模型 Claude 仅用 11 天就“几乎完全自主地”完成了费马大定理（Fermat's Last Theorem）的首个端到端、可由计算机完整核验的形式化证明。在此过程中，Claude 编写了 1300 万行 Lean 代码，并证明了 29,500 个中间定理。
那么，什么是 Lean？
提交方式
提交 Solution.lean
其他内容
本题可以轻松被 Agent 解决，更多用于让大家了解什么是基于 dependent type 的定理证明。
Hello GeekPie_ 2026
- 状态
- 已结束
- 规则
- IOI
- 题目
- 23
- 开始于
- 2026-9-19 0:00
- 结束于
- 2026-10-3 0:00
- 持续时间
- 336 小时
- 主持人
-
Honahec
- 参赛人数
- 227
