Can math AI survive a simple rewording?
- What it is
- The authors introduce a 13-domain benchmark for testing whether theorem-proving systems reason, formalize, and survive harmless rewording.
- Who did it
- Jiaxin Yuan and colleagues
- What it could mean
- Change the wording, keep the math. Does the AI still succeed? This benchmark could expose the gap between genuine mathematical reliability and a system that only looks brilliant on familiar questions.
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
Read the original work
MathAdv: What Theorem Provers Know, Reason, Formalize, and Generalize ↗See the proposed checks
Re-run the Lean verifier against a clean Mathlib workspace; sample transformed-problem equivalences; inspect whether reported completion criteria exclude remaining sorry; reproduce a bounded subset of the published benchmark runs.
No proof docket yet
A docket is the public record of checks and open questions. This paper does not have one yet; the check plan above describes work still to do.
Explore existing proof dockets →
- What it claims
- The authors introduce a 13-domain diagnostic benchmark for natural-language and Lean 4 theorem proving, including reformulation tests, and report that formalization remains a bottleneck and equivalent restatements expose robustness limits.
- Why this could matter
- Can math AI survive a simple rewording? Can an AI prove the same theorem when the wording changes? This benchmark tests theorem provers across 13 areas and finds that many stumble on formalization or equivalent restatements, exposing the difference between genuine robustness and a flattering headline score.
- If it holds up
- Methods: it gives developers a better diagnostic map for building math assistants that generalize across subjects and survive harmless rewording, rather than merely excelling on familiar benchmark formats.
- If it does not
- If transformed problems are not truly equivalent or scoring is leaky, model rankings could mislead research; fixing the benchmark still improves evaluation.
- Impact horizon
- Methods · AI evaluation · Theorem proving · Benchmarks
- Version
- v1, submitted 2026-08-26 07:12:54 UTC.
- Why we tracked it
- Its released JSONL data, Lean verification utility, runners, and preserved result structure offer a concrete reproducibility target for evaluating the distinction between compilation, completion, and semantic interpretation.
- Highest-risk dependency
- Whether each informal/reformulated prompt preserves the intended formal statement and whether benchmark scoring separates kernel acceptance from semantic faithfulness.
- Available artifacts
- The repository provides benchmark JSONL, Lean 4 verification through lake exe repl, task runners, and the released junk-theorem study artifacts.
- Current boundary
- Intake record only; examination not started.