Open Problems Lab

Can selected mathematical open problems be attacked in Lean without letting computational certificates or successful experiments masquerade as deductive proofs? Evidence classes stay separate: source-checked theorem statements, bounded computational certificates, and kernel-verified proofs are three different things. A theorem counts as proved only under a pinned Lean/Mathlib environment with compiler success and a zero-sorry, zero-unauthorized-axiom gate.

Intake is paranoid by design. The source archive is pinned by SHA-256; typed registries cover 15 problem records and 29 prompt variants with seven validation tests. The Lean 4.32.0 layer holds immutable hashes of every target statement, enforces strict import and forbidden-token checks, and carries five adversarial fixture tests meant to catch a cheating prover. Candidate first-slice warmups (small-diophantine, ramsey-book-graphs, hadamard) wait on the benchmark contract.

Honest status: no proof is promoted. The exact Mathlib commit is checked out, but dependency resolution has not yet produced a clean lake-manifest.json / CI gate, so the benchmark contract remains blocked. What publishes here is the gate design and intake discipline; the source archive, Lean worktree, attempt logs, and any unproven scaffolds stay private.