Math Gauge evaluates whether a model can deliver mathematical work as requested: construct proofs and counterexamples, review arguments, turn a natural-language goal into a semantically corresponding Lean project, check research background, extend statements and develop mathematical manuscripts. Its tasks come from mathematical writing and review, examining whether the results hold, respect the given conditions and meet the full requested goal.
The current release is Math Gauge 1.0.0: 25 public and 14 private tasks, covering 39 initial answers across 35 mathematical families, plus three prescribed Lean alignment self-check rounds. Public and private results share one combined score.
Three kinds of mathematical work
- Written proofs: prove a statement, construct a counterexample, or review the assumptions and gaps in an argument.
- Lean: audit formal statements, deliver corresponding projects, and diagnose and repair problems through successive self-checks. Compilation and alignment with the original goal are checked separately.
- Mathematical research: check background claims, attempt theorem extensions, or develop a supplied idea into a manuscript with definitions, arguments and explicit boundaries.
Public and private tasks use the same runner and scoring rules. Model analysis pages list public task scores and link to task statements, original answers, reviews and protocols on GitHub. Private tasks appear through anonymous combined contributions and counts.
Reading the leaderboard
| Metric | What it measures |
|---|---|
| MC · Mathematical Capability | Positive credit for valid mathematical results, including confirmed partial progress. |
| RMC · Reliable Mathematical Capability | Valid work after deductions for unsupported claims and incorrect judgments; the default headline score. |
| SMC · Strict Mathematical Completion | Acceptance against the complete task goal, including the required trajectory for successive self-checks. |
The leaderboard also reports content reliability and complete-goal attainment. Separate boards cover written proofs, Lean and mathematical research, with individual model analysis pages. The cost–score chart uses reference total cost for the retained answers; the time–score chart uses weighted time on five shared everyday tasks. Solid points mean all 39 tasks were submitted normally; hollow points mean fewer were. Shared links retain the language, metric and sorting.
AI review uses Sol 6.1 Max for the full review and Astra 6 Max / Dot for cross-checks, with some human spot checks. The GitHub project documentation describes suite versions, execution conditions, review coverage and interpretation limits.
Design approach
A short proof, counterexample or alternative representation can satisfy a task. A change of mathematical space or language must explain the correspondence and carry its conclusions back to the original problem. This generation of Math Gauge examines how reliably a selected range of calculation, proof and collaborative work can be used under stated conditions. Independently solving open frontier problems is not an entry requirement.
The GitHub repository contains the design rationale, suite structure and reproduction documentation.