# Math Gauge

面向 AI 数学工作交付的评测，覆盖书面论证、Lean 形式化与数学研究，并提供公开榜单和逐题证据。

## Metadata

- HTML: https://glenzli.com/projects/math-gauge/
- Markdown: https://glenzli.com/projects/math-gauge.md
- Collection: Projects
- Language: zh-CN
- Published: 2026-11-10
- Updated: 2026-11-12
- Status: active
- Tags: mathematics, benchmark, evaluation, lean, research

## Content

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

  [查看完整榜单](/benchmarks/math-gauge/?lang=zh)

当前正式版为 **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 项目文档](https://github.com/glenzli/math-gauge)。

## 设计取向

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

设计理念、题库结构与复现文档见 [GitHub 仓库](https://github.com/glenzli/math-gauge)。