Release of Gödel’s Poetry: Open source, recursive prover

Stream: mathlib4

[Kelly Davis]

TL;DR: Open source Lean4 prover that recursively decomposes difficult theorems has been released on PyPI goedels-poetry, GitHub KellyJDavis/goedels-poetry, and is described on arXiv here.

Hi All,

I just released an open source Lean4 formalizer and prover that is mostly targeted for re-use by others. All LLMs it uses are swappable and it:

1. Optionally Auto-Formalizes Statements
   a. Auto-formalizes theorem(s) by default using Goedel-Formalizer-V2-32B
   b. Checks auto-formalization syntax using a Kimina Server variant
   c. Checks auto-formalization semantics using qwen3:30b
   d. Repeats the process a configurable number of times until success

2. Proves Formal Statements
   a. Proves theorems using verifier-guided self-correction, Goedel-Prover-V2:32b, and a Kimina Server variant
   b. Theorems resistant to the first step are decomposed into simpler, entailing propositions using GPT-5, qwen3:30b, and a LeanExplore variant
   c. Proofs of entailing propositions are attempted as in the first step
   d. Entailing propositions resistant to proof are recursively decomposed

All the LLMs used can be swapped out for alternatives using environment variables.

It’s able to be used on the command line for single theorems

goedels_poetry --informal-theorem "Prove that the sum of the first n natural numbers equals n(n+1)/2"

or in batch mode

goedels_poetry --formal-theorems theorems/minif2f/

or via its API.

Discussions and or questions should be directed here.