AI Finds, Lean Checks

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.