带输入的代表验收样例
固定实数不等式的Lean证明
对固定的实数不等式，检查证明编译及传递公理，不用数值例子替代证明。
仅合成练习的验收器校准；没有新AI试次或一般成功率。
验收方法实际检查到了什么
参考解与合理替代均被接受，关键错误被拒收。 负控制拒收 7 项；校准控制共 9 项。
这是验收器校准，新增模型调用 0 次；未产生本工作单元的AI成功率。
- 仅合成练习的验收器校准；没有新AI试次或一般成功率。
- 固定命题与允许公理下的证明检查；形式化题意另需核对。
下载输入、规则与验收资产
含校准脚本与所需本地评分器。代码隔离需要Linux用户/挂载/网络命名空间；数学需另准备包内锁定的Lean与Mathlib版本。
先读契约和输入，再尝试作答。参考解用于校准，不应混入模型试验输入；运行前查看各包说明与环境要求。
# 固定命题证明：W-M01 验收示例 v1.0.0 命题：对任意实数x、y，2xy≤x²+y²。固定形式签名、Lean 4.19.0与Mathlib commit见input.json。这里选择已固定的可重放版本，不声称它是最新版本。提交仅proof body，以by开始；运行器注入不可变的声明、所需import和#print axioms。允许的基础公理仅propext、Classical.choice、Quot.sound；不允许sorry/admit、额外假设、修改声明、增加公理、native_decide、代码执行型元编程。 参考用(x-y)²≥0，替代用(y-x)²≥0。空文件、占位证明、类型不符、改命题和额外公理均应被拒。核验同时检查实际内核编译与传递公理清单；形式命题与中文题意仍需接收者核对。返回未找到证明不能改写为命题不成立。 复跑：准备指定revision的Mathlib及缓存，以python3 scripts/check-work-unit-examples.py --lean-project PATH --lean-bin PATH/bin运行。未配置内核时必须记environment_blocked，不允许把字符串检查写成数学证明通过。整个包为验收器校准，没有新模型试次、没有一般数学成功率。 本代表校准采用明确受限的证明语法：by、have、show/from、exact、calc、nlinarith、sq_nonneg、rfl、le_refl、le_of_eq、pow_two、ring_nf，变量x/y及h编号局部引理；拒绝其它标识符、注释、字符串和额外命令。超出语法返回unsupported_submission，表示需要改用更完整且隔离的证明运行器，不表示数学命题或证明错误。随后仍实际编译并检查传递公理。追加lemma或initialize也必须在执行前拒绝。
参考解、合理替代与已知错误控制
资产版本和SHA256
2026-10-19.examples.1
alternative.lean · 163206fe313886ea52526655e683e2e3d8d5d550e55d854357ea80870119b9d5
contract.md · 33b0575953e78190740e218105cece6a919c2d83a1e1ad083af430a9cdbb60e1
controls/changed-statement.lean · 50dd677de023dccfd4ce41191f4f6f536532d4b894de6b20de0acc8e2abdba6d
controls/extra-axiom.lean · fc18442c65688b914f4f9073dd22171ae2d03da697b0b1f9ce4a8a84b798ecfd
controls/extra-lemma.lean · 48982a29cbc8e2b436763a15398cb5811a8ce5b634e634f95f63101e0171acca
controls/false-proof.lean · 10c9e2e82653a2fb61531d495f1b8eaee8d135952098e72979e87adda51033c3
controls/initializer.lean · f299d1018ee8f5a357cc97c5e0044a09e9a733fc2ca3eed68ad37a5027af456c
controls/noop.lean · e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855
controls/sorry.lean · 26f51390193316d1028961c80d7baaf642386f80da2a233c3fac01e555d0c6dd
input.json · c00bb1c87275cfb1baca4e41e419e5c26446d5fe80790a99e2c3dd8658e82f52
lean-toolchain · 55e97be96000b5e9e290c9e74482e5e317861499a5540353ce845471bded8cea
reference-result.json · 99ebda99694c56272dbec1e02891d545ff7da23ec96f3b6736c9b1c4de12561c
reference.lean · 0ffdda9474ed340642b8f06a469a35f1bc26d7f195055fa69af8866a68ae9c7c