AxQM：一种用于有限维量子力学库中形式化证明合成的标准规模基准测试』

AxQM 基准于 2026 年 9 月 7 日发布，旨在评估形式化证明合成能力。该基准包含来自《量子计算与量子信息》教材的 1019 个可验证任务，规模约为现有水平的四倍。所有任务均源自对教材正式部分的完整形式化，并基于自定义的有限维量子力学 Lean 库构建。解决方案保持私有，评分由 Lean 内核执行确定性检查，确保证明编译通过、无 sorry 声明且不引入新公理。