Blueprint-based theorem proving—planning the proof structure upfront before solving individual lemmas—is more efficient than recursive decomposition and enables solving hard competition math problems with open-source models at low cost.
Goedel-Architect is an AI system that proves formal mathematical theorems in Lean 4 by first generating a blueprint—a dependency graph of definitions and lemmas needed for the proof—then solving each lemma in parallel.