Gödel's Poetry: AI, Lean 4 Prover
A Lean 4 multi-agent theorem proving system combining recursive decomposition, RAG-based retrieval, AST extraction, and verifier-guided proof generation.
A Lean 4 multi-agent theorem proving system combining recursive decomposition, RAG-based retrieval, AST extraction, and verifier-guided proof generation.