Math Gauge

Math Gauge 检验模型能否按题意完成数学工作：构造证明与反例、审阅论证、把自然语言目标落实为语义对应的 Lean 工程，以及核查研究背景、拓展命题和整理数学手稿。评测从数学写作与审阅中的实际任务出发，关注成果是否成立、是否忠实于条件，以及整项工作交付到了哪一步。

当前正式版为 Math Gauge 1.0.0：公有 25 题、私有 14 题，合计 39 道初答与 35 个数学题族；另有 3 轮固定 Lean 对齐自查。公私结果合并计分。

三类数学工作

• 书面证明：完成证明、给出反例，或审阅一份论证中的条件与缺口。
• Lean：核查形式命题的语义、交付对应工程，并在连续自查中诊断和修补问题。编译通过与证明了原目标分别检查。
• 数学研究：核查背景，尝试拓展命题，或把给定想法写成有定义、论证和边界的数学手稿。

公有与私有题库使用同一套运行器和评分规则。模型分析页列出公开逐题成绩，题面、原答、评审和协议链接到 GitHub 查看；私有题以匿名合并贡献和数量展示。

怎么读榜单

指标	衡量内容
MC · 数学能力	有效数学成果的正向贡献，包含可确认的部分进展。
RMC · 可靠数学能力	在有效成果上扣除错误承诺、误判等损失，是默认主分。
SMC · 严格数学交付	按整题目标验收；连续自查还检查规定轨迹的完整性。

榜单同时展示内容可靠率与完整目标达成率，可分别查看书面证明、Lean 和数学研究分榜，并进入单个模型的分析页。成本—成绩图使用留档作答的参考总成本，耗时—成绩图使用共同日常五题的加权耗时。39 题均正常交卷的模型显示为实心点，其余为空心点。语言、口径和排序可随链接分享。

当前结果由 AI 审核：Sol 6.1 Max 全审，Astra 6 Max／Dot 抽审核对，并有部分人工抽审。题包版本、运行方式、审核覆盖和结果解释见 GitHub 项目文档。

设计取向

有效的短证、反例和替代表示都可以完成目标；换一种空间或语言时，需要交代对应关系，并把结论带回原问题。Math Gauge 的这一代题包考察一部分计算、证明与协作能力在明确条件下能否稳定使用，独立攻克前沿未解问题不作为必要门槛。

设计理念、题库结构与复现文档见 GitHub 仓库。