数学验证中心
AI 负责讲题，验证器负责阻止未经证明的数学结论被标成“已验证”。当前正式收录 16 道通过固定版本 Lean + Mathlib 的竞赛题。
Formally Verified ≠ AI 自评正确只有保存的形式化命题在固定工具链上重新运行通过，才显示该标识。
我们验证什么
验证对象是数学命题本身，而不是页面文案。每条记录绑定证明源文件指纹、Lean 工具链、Mathlib revision、验证器代码 revision 和时间戳。证明源码一旦变化，指纹随之变化，旧验证记录不能继续冒充当前证明。
AUDIT LOG
返回数学训练指南形式验证记录
题目方法领域LeanMathlib证明指纹
maa-amc10-2022-a-sample-q02AMC 10A · 2022Lean 形式验证arithmeticv4.34.1d13f23b723b8…9eedcf9fdd0c…
maa-amc10-2022-a-sample-q03AMC 10A · 2022Lean 形式验证algebrav4.34.1d13f23b723b8…9eedcf9fdd0c…
maa-amc10-2022-a-sample-q04AMC 10A · 2022Lean 形式验证algebrav4.34.1d13f23b723b8…fc8379592f47…
maa-amc10-2022-a-sample-q06AMC 10A · 2022Lean 形式验证algebrav4.34.1d13f23b723b8…fc8379592f47…
maa-amc10-2022-a-sample-q07AMC 10A · 2022Lean 形式验证number_theoryv4.34.1d13f23b723b8…fc8379592f47…
maa-amc10-2022-a-sample-q08AMC 10A · 2022Lean 形式验证number_theoryv4.34.1d13f23b723b8…9eedcf9fdd0c…
maa-amc10-2022-a-sample-q10AMC 10A · 2022Lean 形式验证geometryv4.34.1d13f23b723b8…2c02139d514d…
maa-amc10-2022-a-sample-q12AMC 10A · 2022Lean 形式验证combinatoricsv4.34.1d13f23b723b8…2c02139d514d…
maa-amc10-2022-a-sample-q16AMC 10A · 2022Lean 形式验证algebrav4.34.1d13f23b723b8…fc8379592f47…
maa-amc10-2022-a-sample-q17AMC 10A · 2022Lean 形式验证number_theoryv4.34.1d13f23b723b8…2c02139d514d…
maa-amc10-2022-a-sample-q18AMC 10A · 2022Lean 形式验证geometryv4.34.1d13f23b723b8…2c02139d514d…
maa-amc10-2022-a-sample-q19AMC 10A · 2022Lean 形式验证number_theoryv4.34.1d13f23b723b8…2c02139d514d…
maa-amc10-2022-a-sample-q20AMC 10A · 2022Lean 形式验证algebrav4.34.1d13f23b723b8…272d76c52f96…
maa-amc10-2022-a-sample-q24AMC 10A · 2022Lean 形式验证combinatoricsv4.34.1d13f23b723b8…2c02139d514d…
maa-amc8-2024-q01AMC 8 · 2024Lean 形式验证arithmeticv4.34.1d13f23b723b8…fc8379592f47…
maa-amc8-2024-q03AMC 8 · 2024Lean 形式验证geometryv4.34.1d13f23b723b8…fc8379592f47…