01 / ACQUIRE
Anchor the theorem.
Read the authentic IMO source; preserve every quantifier and hypothesis.
PROJECT RIGOR MORTIS // MATHEMATICAL PROOF FORENSICS
Make the
argument
confess.
Beautiful proofs can conceal a single fatal inference. Find it. Explain it. Repair it. A forensic laboratory built around the mathematics of the International Mathematical Olympiad.
19IMO CASE FAMILIES
111PROOF AUTOPSIES
120OFFICIAL IMO LINKS
111 project-authored proof fragments, including 90 new advanced cases. Author labels are learning references, not independent expert adjudication.
DETECTION / FIRST FALSE INFERENCEREPAIR / MATHEMATICAL NECESSITYEVIDENCE / SOURCE-LINKED IMOSTATUS / PUBLIC PRACTICE · LOCAL ONLY
THE FORENSIC PROTOCOL / 4 PHASES
02 / ISOLATE
Trace the argument.
Mark the first unsupported inference, not just a wrong final answer.
03 / RECONSTRUCT
Repair the gap.
Write a counterexample, missing lemma, or mathematically sound replacement.
04 / AUDIT
Export evidence.
Download a local proof dossier for teacher inspection or research discussion.
01 / INTERACTIVE PROOF FORENSICS
Every line is
a suspect.
Nineteen sourced IMO families, 111 authored proof fragments, multiple clean controls, and subtle near-miss inferences. Choose a case, audit the logical chain, and assemble an exact repair.
RIGOR_OS /lab · FORENSIC WORKSTATION
19 FAMILIESCASE 01 / 111
CASE NAVIGATOR // EXPERT COLLECTION
Find a proof worth doubting.
Search all 111 individual autopsies by IMO year, mathematical technique, theorem or title. Download a ten-case seminar deck with no answer key.
111 cases in the collection
MATHEMATICAL EVIDENCERESEARCH
CASE NOTE: Some fragments prove only intermediate lemmas, not the entire Olympiad problem. CLEAN means the displayed fragment is valid under its stated hypotheses; it is not a certification of a full IMO solution.
INVESTIGATION DOSSIER
LOCAL MODELocate. Diagnose.
Reconstruct.
TRAINING MODE
Reference analysis stays hidden until you turn off the label-hiding control. Select the earliest unsupported inference or CLEAN.
CASE WORKFLOWSELECT → DIAGNOSE → REPAIR → EXPORT
0 / 3 required steps completed
Important: classroom label-hiding is a UI convenience, not cryptographic blinding. Author keys are shipped to the browser for optional feedback. These cases cannot be used as an unseen research holdout.
02 / SOURCE LIBRARY
A lifetime of
unresolved beauty.
One hundred and twenty links to the official 2006–2025 IMO problem papers. The curated lab concentrates on 19 especially instructive source problems. Archive entries without curated cases are linked references, not full solutions.
03 / OLYMPIAD COACHING STUDIO
Built for people who
don't accept hand-waving.
Author a new high-level proof audit, teach with concealed feedback, and save reasoning as a local JSON packet. The professor controls adjudication.
NEW · PROFESSOR'S PROTOCOL / v5.0
Design an adversarial seminar.
Balanced valid controls and subtly flawed proofs. Choose a track, repeatable seed and case count. Generate a student booklet plus a separate author-labelled reference guide — no participant data leaves this browser.
DETERMINISTIC SELECTION · NO CLOUD
Choose options and generate a mathematically balanced practice set.
NEW · LOCAL CASE INGESTION
Bring your own proof.
Import a classroom packet generated below, then audit it inside the same live workstation. Imported files stay on your device and have no automatic truth label.
No local packet loaded
PROTOCOL A / CREATE A CASE
Author a forensic packet.
PROTOCOL B / DEPENDENCY VISUALIZER
Find where the logic breaks.
Each dossier includes the original theorem context, all proof steps, a selected fatal-step diagnosis, an explicit repair attempt, and the associated source. Exports contain no server secrets or private ground-truth keys.
Teacher packets are ungraded local documents. Not a server-side reviewer workflow or an automated proof certification service.
06 / EXPERT PROOF REVIEW · TWO-SIDED WORKFLOW
Don't just grade.
Audit the reasoning.
A student exports a forensic dossier. A mathematical mentor imports it, evaluates the first fatal step, assesses the obstruction and the repair, and returns a structured review file. Genuine review decisions remain human-authored.
01 / STUDENTExport a proof dossier from the Laboratory
02 / INSTRUCTORRead the full mathematical reasoning and score each dimension
03 / FEEDBACKReturn a portable report that the student can open locally
A / REVIEW INTAKE
Open an audit dossier.
Select a JSON file previously exported from any public RIGOR proof autopsy. The mathematical work is read only on your device.
No dossier imported.
Author reference is optional and is NOT expert adjudication.
B / MATHEMATICAL RUBRIC
Evaluate four obligations.
Every dimension is scored manually from 0 to 4. A high score means the reviewer believes the written argument meets the criterion; it is not a verified AI metric.
Does the learner identify the earliest unsupported inference rather than a later consequence?
Is there a rigorous counterexample, a missing hypothesis or a precise reason the inference fails?
Does the proposed replacement prove what is needed, with domains and quantifiers intact?
Are definitions, dependencies and use of assumptions logically transparent?
HUMAN-ASSESSMENT TOTAL— / 16
“Signed-off” means a named human-authored report, not a cryptographic signature or institutional endorsement.
C / STUDENT FEEDBACK VIEWER
Read your instructor's critique.
Open a feedback JSON file that a teacher exported from the review station. Nothing is uploaded and no identity is verified by the website.
No feedback report loaded.
RESEARCH INTEGRITY: This public workstation is not the private v43 blind-review system. A public author answer key is accessible within the browser. Human scoring, file exchange and references are not independent experimental adjudication. Students should not import sensitive personal information.
04 / OPEN RESEARCH NOTEBOOK
The scientific claim is
the inference itself.
RIGOR MORTIS investigates the structural difference between correct and persuasive-but-invalid mathematical reasoning. The public lab is deliberately distinct from private participant data and unreleased blind-review infrastructure.
CONTRASTIVE VALIDITY
One step. Two worlds.
Hold the theorem and proof context stable while testing whether a changed step alters mathematical validity. Guard against template-only recognition.
CALIBRATION LEAKAGE
44 labels ≠ 44 proofs.
Previously archived author-labelled calibration data permitted sibling-label shortcut reconstruction. This is an evaluation-design flaw, not proof-verification efficacy.
REPAIR, NOT JUST VERDICT
Counterexample → lemma.
Judge whether a diagnosed gap can be repaired into an actually valid argument. A label is not a proof, and a fluent explanation is not certification.
STATUS DISCLOSURE. Research preview, not peer-reviewed. These 111 items contain project-authored answers, not independently expert-adjudicated results; substantial AI assistance was used in constructing this public release. No participant numbers, external endorsements, verified AI score, or live blind-review workflow are claimed. The browser demo does not collect submissions.
05 / PUBLIC MATHEMATICAL VERIFICATION
Trust is earned
one invariant at a time.
Reproducible finite checks for selected underlying mathematical claims. Each result is backed by a downloadable standard-library Python script and a machine-readable verification manifest.
∑
IMO 2019 / P51,022Enumerated starting states. Exactly decreasing potential and expected move count.
PASS · STATE ENUMERATIONƒ
IMO 2024 / P618,225Exact rational pairs for the two-branched functional equation.
PASS · EXACT FRACTIONSℤ
IMO 2006 / P57,218Integer-polynomial difference divisibility tests.
PASS · DIVISIBILITY⊗
IMO 2007 / P69Binomial-weight moment families for Lagrange annihilators.
PASS · EXACT MOMENTSREPRODUCIBLE EVIDENCE
Also verified: 401 adjacent-gcd identities for IMO 2016 P4. These finite tests do not validate every case label; they are an inspectable supplement to mathematical review.