题目

自然数加法小题 · Lean 标准库

候选

先提交一份失败候选，再提交修复后的证明

模型

不调用模型，不需要 API Key

验收

完整原题由独立 Lean 流程检查

这份回放展示 TheoremOS 怎样记录候选、检查与修复，并以完整原题的 evaluated_passed 作为验收结论。在线工作台开放后，可以在浏览器中运行自己的题目。