Goedel-Prover

Stream: Machine Learning for Theorem Proving

[Eugene]

I came across a new paper from Sanjeev Arora and team "Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving". Several interesting claims. Efficient autoformalization from Numina to Lean 4. SOTA on miniF2F, etc.

They claim that the code is open sourced, but I only see the testing code in the repository. Weights are available too.

I don't understand example 2 in table 1, though. The informal statement looks wrong.

[Yong Lin]

Hi, thank you for your interests in our Goedel-Prover. We do not include for the training code since it is standard supervised fine-tuning and we use a standard package "trainner from Transformer".

[Yong Lin]

There is a typo in example 2 in table 1, it should be $0<x<1$

[Amitayush Thakur]

@Eugene : If you are looking for training code specific to theorem proving (single proof-step/tactic prediction), then you can check out our repository: https://github.com/trishullab/proof-wala (it also comes with search capabilities that can run in parallel). Although we don't have expert iteration training which I guess was used in Goedel-Prover. I don't think there is any "Open Source" expert iteration training code in the context of theorem proving.

[V S]

Has anyone been able to set up Goedel-Prover locally? Due to technical constraints, I was unable to do so, but I'm quite interested in its results and various prompts it could work with. Am I correct in assuming that the open-source version of Goedel-Prover can take any mathematical problem (that is, the problem in english, it's formalization to Lean, including the header, and name,id,etc) and attempt to solve it? What will be the outcome if Goedel-Prover cannot solve it? How is it summarized exactly in compilation_summarize.json?