Gödel’s Poetry

We introduce a new approach to computer theorem proving, employing specialized language models for Lean4 proof generation combined with recursive decomposition of difficult theorems into simpler entailing propositions. These models are coordinated through a multi-agent architecture that orchestrates autoformalization (if required), proof generation, decomposition, and recursive proof. Without decomposition, we achieve a 90.4% pass rate on miniF2F; with decomposition, this is significantly improved. A key technical contribution is our extension of the Kimina Lean Server with AST parsing capabilities for automated, recursive proof decomposition. The system is available on PyPI as goedels-poetry and open-source at KellyJDavis/goedels-poetry.

Recommended citation: Kelly Davis. (2025). "Gödel's Poetry." arXiv Pre-print.
Download Paper