# Proof Atelier

- **Event:** [Meta Global AI Developer Hackathon](https://cerebralvalley.ai/e/meta-ai-developer-hackathon)
- **When:** Oct 26, 12:00 PM – Nov 4, 9:00 PM (EST)
- **Where:** Online
- **Team:** [Conor Hale](https://cerebralvalley.ai/u/ConorHale)
- **GitHub:** https://github.com/Conorhale/Proof-Atelier-Hackathon-2026
- **Demo video:** https://proof-atelier-conor.conorhale07.chatgpt.site/Proof-Atelier-Demo-v2.mp4
- **Gallery:** https://cerebralvalley.ai/e/meta-ai-developer-hackathon/hackathon/gallery
- **Page:** https://cerebralvalley.ai/e/meta-ai-developer-hackathon/hackathon/gallery/1606

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.

## More from Meta Global AI Developer Hackathon

- [1853974242455090/Jeano Joseph Vincent](https://cerebralvalley.ai/e/meta-ai-developer-hackathon/hackathon/gallery/1603)
- [Ivan Romanteyev (solo dev)](https://cerebralvalley.ai/e/meta-ai-developer-hackathon/hackathon/gallery/1604)
- [Behtafood](https://cerebralvalley.ai/e/meta-ai-developer-hackathon/hackathon/gallery/1605)
- [aadhaa](https://cerebralvalley.ai/e/meta-ai-developer-hackathon/hackathon/gallery/1607)
- [Anubhav](https://cerebralvalley.ai/e/meta-ai-developer-hackathon/hackathon/gallery/1608)
- [FEN meta synthesis](https://cerebralvalley.ai/e/meta-ai-developer-hackathon/hackathon/gallery/1609)

---

Markdown version of https://cerebralvalley.ai/e/meta-ai-developer-hackathon/hackathon/gallery/1606. Site index for agents: https://cerebralvalley.ai/llms.txt · full text: https://cerebralvalley.ai/llms-full.txt