Gödel’s Poetry is a Lean 4 theorem proving project that combines AI-based proof generation with recursive decomposition, retrieval-augmented theorem search, and verifier-guided proof reconstruction.
The project explores how modern language models, formal proof assistants, and multi-agent architectures can work together to prove mathematical statements in Lean.
Key components include:
- Lean 4 proof generation
- recursive theorem decomposition
- RAG-based theorem retrieval
- AST-based subgoal extraction
- proof verification via Lean tooling
Related blog post: