A proof checker can accept the wrong question
- What it is
- A paper tests a way to translate ordinary mathematical questions into Lean statements while checking whether the meaning survived.
- Who did it
- Thomas Hirtz, Farzad Jafarrahmani, Abdelmouksit Sagueni, Xiang Zhou, Wenping Deng, and Liang Zhang.
- What it could mean
- If the method proves reliable beyond its tests, formal proof projects may catch a dangerous error earlier: checking a perfectly typed statement that asks the wrong question.
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
Sage: Formalization with Semantic Correction ↗See the proposed checks
Separate answer-aware/agnostic regimes and pass@1/pass@4; examination a fixed informal/formal sample for missing hypotheses, changed bounds, vacuity, and answer injection.
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 →
Did the translation keep the same question?
The matching shapes suggest preserving a mathematical statement while translating it into a formal language. Sage checks statement fidelity; the illustration does not show a proved theorem or a verified benchmark outcome.
Read the source · Sections 3–4 · statement formalization and semantic correction ↗- What it claims
- A four-stage translation and model-based correction loop reportedly reduces answer leakage in stated evaluations. Compilation uses a single sorry placeholder and does not prove the target. The authors report 71.1% agreement in a 45-case stratified human examination. This is intake of the revised v2 source.
- Why this could matter
- A proof checker can accept the wrong question Lean can verify that a statement is well formed without knowing whether it matches the mathematician's original problem. Sage adds semantic review to the translation step and reports fewer guessed answers in its tests.
- If it holds up
- It could improve the quality of formal problem statements supplied to proof assistants, while leaving proof and semantic judgment as separate tasks.
- If it does not
- Judge disagreements or leaked answers would expose which translation checks still let a wrong formal question look credible.
- Impact horizon
- Methods · Autoformalization · Formal mathematics · AI-assisted proof workflow
- Version
- revised 2026-09-30 11:57:05 UTC; v1 submitted 2026-09-16 17:17:13 UTC
- Why we tracked it
- unexamined proof-method intake, not a validated semantic gate or homepage feature.
- Highest-risk dependency
- Model-based semantic judgment is not kernel verification; human-examination agreement is limited, and existential targets can admit proof shortcuts.
- Available artifacts
- arXiv v2 PDF/HTML/TeX available; no pinned implementation repository established in this pass, and no code/corpus run.
- Current boundary
- Intake record only; examination not started.