Proof Atelier

Proof Atelier helps university students find the first unsupported step in a mathematical argument, understand the gap, and export a Lean certificate for the exact formal theorem they intended to prove. A plausible proof can hide a missing constant or a misused induction hypothesis. Proof Atelier turns a structured argument into a dependency graph. Lean checks each claim using only the original assumptions and its declared verified predecessors. A failed claim blocks downstream steps. Students see a hint before a reference correction, and review the statement, assumptions and candidate steps before adopting a repair. Adoption clears the old verification result. Only a complete theorem that passes Lean and the axiom audit receives a certificate. The event-period work extends a pre-existing 22 October prototype with named induction/case validation, finite sums and higher-level examples, formal-target preservation, the official Meta Model API adapter, explicit AI-repair provenance, a bounded compiler-feedback evaluator, expanded tests and Docker distribution. The supported fragment includes induction, abstract rings, set identities, real arithmetic, continuity, composed derivatives and determinants. Evidence: CI passed 176 tests, with 2 optional media-test skips. All 14 curated flawed examples failed as expected; all 14 reference corrections verified and their certificates recompiled independently. Docker was tested with a non-root process, read-only filesystem and networking disabled for certificate export. These are regression results, not general proof accuracy or measured learning gains. Public CI runs: https://github.com/Conorhale/Proof-Atelier-Hackathon-2026/actions/runs/41763324101 and https://github.com/Conorhale/Proof-Atelier-Hackathon-2026/actions/runs/41763323972. Try the public workspace, demo and evidence: https://proof-atelier-conor.conorhale07.chatgpt.site/submission The website replays actual recorded Lean checks and needs no login. The downloadable application checks new proofs locally. The 2-minute-56-second captioned video uses actual browser captures and reference corrections, not live AI. No live Meta-model evaluation or student study is claimed. Human review of natural-language alignment remains necessary. Pre-event work, the original MIT license and Codex assistance are disclosed.