Project: Gödel's Poetry
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 GitHub repository Related blog post: ...