Matched counterfactuals
One near-miss can replace a single inference while leaving the theorem and the remainder of the proof unchanged. Validity-preserving control edits are essential to distinguish proof checking from mutation spotting.
01 / THE SCIENTIFIC TARGET
The earliest unsupported inference
A valid conclusion is not enough. Given a theorem T and a step-numbered proof P=(s₁,…,sₖ), the evaluator must identify the first unjustified line or return CLEAN. Exact localization is compared against independently adjudicated mathematical reference labels. Abstentions, malformed predictions and ambiguity must not disappear from denominators.
Family-aware evaluation
Whole theorem families, not individual proof versions, must be held out. The 111 public training cases are exposed and cannot be reused as unseen evaluation items.
02 / LEAKAGE CALIBRATION
Correct labels for the wrong reason.
The research-analysis implementation v4 rejects unknown evaluation exposure, unadjudicated evaluation cases, out-of-range indices, and every colliding receipt or participant–case record, rather than silently selecting whichever answer appears first. These are software safeguards, not real participant results. The archived calibration set consisted of 44 active author-labelled items across 12 families. Exactly two labels per active family were VALID. Given this family quota and every other sibling's labels, the final verdict can be reconstructed without any proof reading:
zᵢ = r − Σj∈F, j≠izⱼ
This is an exact logical shortcut under known sibling labels and quotas, not evidence that a real deployed model used that shortcut. It predicts binary verdicts, not the first invalid step. The archived data and full calibration numbers have not been independently replicated from raw source material for this release.
03 / EXACT MATHEMATICAL CASE STUDY
A constructive theory of finite-increment repair
Motivated by IMO 2011 Problem 3, consider nonnegative g:(0,∞)→[0,∞) with:
g(s+t) ≥ t·g(s), s,t>0.
For the anchored minimal construction, the parameter C is nonnegative, including C=0 (where the anchored function is identically zero). This closes a boundary case in the finite-interval feasibility argument.
Its sharp subdivision envelope is K(T) = maxm≥1(T/m)m. Equal increments and concatenation give K(u+v)≥K(u)K(v). Any admissible function satisfies:
g(a+T) ≥ K(T)g(a).
At ordered anchors a₁<…<aₙ, define Wᵢⱼ=K(aⱼ−aᵢ) for i<j and Wᵢᵢ=1. Finite intervals Lᵢ≤g(aᵢ)≤Uᵢ admit a finite-valued admissible extension if and only if LᵢWᵢⱼ≤Uⱼ for every ordered pair i≤j.
Least upward-only repair
vⱼ = maxi≤j cᵢWᵢⱼ
This coordinatewise least admissible anchor vector above initial observations cᵢ≥0 is realized by the pointwise maximum of minimal anchored admissible functions. It is not necessarily the unique full-domain extension.
Weighted symmetric correction
ε* = max{0, maxi<j(Wᵢⱼcᵢ−cⱼ)/(Wᵢⱼqᵢ+qⱼ)}
For anchors (1,2,3), c=(1,1,1), q=(1,1,1), upward-only gives (1,1,2). The symmetric minimax example gives ε*=1/3 and one optimal vector (2/3,2/3,4/3). Written proofs and a reproducible rational test script accompany the full LaTeX manuscript; 9,417 exact-rational finite checks passed. Finite tests are not universal proofs or independent mathematical review.
04 / EVIDENCE BOUNDARY
What we have — and have not — measured.
| Component | Verified | Not established |
|---|---|---|
| Website & public cases | Live browser-visible practice with 111 author labels; 120 official IMO links | Independent mathematical adjudication or true unseen benchmark |
| Private backend | Synthetic write/read/delete on Vercel Blob | Approved human intake, complete reviewer E2E and abuse/retention controls |
| Calibration | Family quota reconstruction identity | Current validated raw outcomes or model efficacy |
| Human participants | No actual study results claimed | Recruitment, response statistics, effect sizes, participant affiliations |
RESEARCH INTEGRITY. This is a non-peer-reviewed working manuscript. The public casebook and structural audit are open for inspection; they are not expert proof validation. No adopted paper, DOI, independent expert authorship, human performance, verified adoption, or experimental outcome is claimed. The private participant intake remains CLOSED.
05 / STUDY AND EXPERIMENTAL PROTOCOL
How to make the next result defensible.
Independent adjudication
Two mathematicians per unseen item; a third adjudicator or quarantine for disagreement; frozen case version, first-error key and proof repair explanation before exposure.
Contamination control
Family-disjoint development and evaluation data. Compare matched clean, invalid and validity-preserving edits. Pre-specify all item exclusions and model-prompt settings.
Responsible participants
Voluntary adult-only pilot after adequate GDPR information, appropriate ethical review, authorization and tested deletion. Do not recruit minors through AoPS or collect usernames.
Evidence-rich analysis
Report exact first-step localization, false-CLEAN, false criticism, expert disagreement, repair sufficiency, clustered uncertainty and how participant backgrounds were verified.
06 / RELATED WORK
Where RIGOR fits
Hard2Verify (ACL 2026) evaluates step-level mathematical verification. ProofBench and ProofGrader (ICLR 2026) address fine-grained proof grading. RIGOR's prospective differentiator is combining first-error location with mathematically verified repair, matched proof polarity controls and family-aware leakage protection. Priority over existing work is not claimed.
VERSIONED STUDY PROTOCOL ↗ · PUBLIC STRUCTURAL AUDIT / CASEBOOK ↗ · FINITE TEST MANIFEST ↗ · HUMAN PROOF REVIEW WORKBENCH ↗