# AI Finds, Lean Checks

- **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:** [Srinath Pulagalla](https://cerebralvalley.ai/u/srinath187)
- **GitHub:** https://github.com/Srinath171/ai-finds-lean-checks
- **Demo video:** https://drive.google.com/file/d/14Y68pV_JLhGJGpDdGKpyaLELzXbCnA0h/view?usp=sharing
- **Gallery:** https://cerebralvalley.ai/e/meta-ai-developer-hackathon/hackathon/gallery
- **Page:** https://cerebralvalley.ai/e/meta-ai-developer-hackathon/hackathon/gallery/5239

AI Finds, Lean Checks is a local proof and finite-search laboratory inspired by the gap between finding and checking solutions. Muse Spark 1.3 and Muse Wonder 1.0 propose Lean 4 proof bodies for fixed theorem statements. A restricted checker screens the proof, runs Lean, audits the axioms, and returns diagnostics to the model for bounded retries. A Streamlit interface exposes attempts and verdicts, with reproducible logs and a model comparison.

On the same 15 elementary theorems at maximum effort, both models achieved 15/15 recorded verified results: Wonder used 15 attempts and Spark 16. Recorded token-based benchmark cost estimates were approximately $0.102 and $0.087 respectively, not total project costs or invoices. The lab also formalizes SAT-search correctness, the exact four-NAND-gate bound for XOR in a stated circuit model, and a known counting argument for the existence of hard Boolean functions. The latest saved checkpoint records 34 cumulatively compiled Lean modules and 475 passing Python tests.

The contribution is the generate-check-repair pipeline, its verification controls, and inspectable experiments. It does not solve P vs NP or claim new mathematical discoveries. Experimental research proposals remain unverified unless separately checked. Public source and local run instructions are included in the repository.

## More from Meta Global AI Developer Hackathon

- [AMADEUS](https://cerebralvalley.ai/e/meta-ai-developer-hackathon/hackathon/gallery/5236)
- [Cache Me If You Can](https://cerebralvalley.ai/e/meta-ai-developer-hackathon/hackathon/gallery/5237)
- [Sourcebound](https://cerebralvalley.ai/e/meta-ai-developer-hackathon/hackathon/gallery/5238)
- [Helpious AI](https://cerebralvalley.ai/e/meta-ai-developer-hackathon/hackathon/gallery/5240)
- [Folkstyle arena](https://cerebralvalley.ai/e/meta-ai-developer-hackathon/hackathon/gallery/5241)
- [Open Idea](https://cerebralvalley.ai/e/meta-ai-developer-hackathon/hackathon/gallery/5242)

---

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