Goedel-Architect: Streamlining Formal Theorem Proving with Blueprint Generation and Refinement 事件

Goedel-Architect: Streamlining Formal Theorem Proving with Blueprint Generation and Refinement arXiv:2606.06468v1 Announce Type: new Abstract: We introduce Goedel-Architect, an agentic framework for formal theorem proving in Lean 4 centered on blueprint generation and refinement. A blueprint is a dependency graph of definitions and lemmas that builds up to the main theorem. First, Goedel-Architect generates a blueprint of formally stated definitions and lemmas, along with declared dependencies.