Discussion: Goedel-Prover-V2: A new SOTA model

Stream: Machine Learning for Theorem Proving

[Kelly Davis]

Yong Lin said:

The Goedel team is happy to annouce our open sourced SOTA model Goedel-Prover-V2.

Our flagship model, Goedel-Prover-V2-32B, achieves the new SOTA...

All in 32B! Impressive! :clap:

Are there plans for an arXiv paper?

[Notification Bot]

A message was moved here from #announce > Goedel-Prover-V2: A new SOTA model for theorem proving by Matthew Ballard.

[Yong Lin]

Kelly Davis said:

Yong Lin said:

The Goedel team is happy to annouce our open sourced SOTA model Goedel-Prover-V2.

Our flagship model, Goedel-Prover-V2-32B, achieves the new SOTA...

All in 32B! Impressive! :clap:

Are there plans for an arXiv paper?

Arxiv paper is coming in 2-3 weeks.

[Notification Bot]

A message was moved here from #announce > Goedel-Prover-V2: A new SOTA model for theorem proving by Matthew Ballard.

[Kaiyu Yang]

Should we move the discussion to #Machine Learning for Theorem Proving ?

[Kelly Davis]

Kaiyu Yang said:

Should we move the discussion to #Machine Learning for Theorem Proving ?

Yes. It seems a more appropriate home.

[Kaiyu Yang]

@Matthew Ballard Could you please help us move the discussion? Thanks!

[Notification Bot]

This topic was moved here from #general > Discussion: Goedel-Prover-V2: A new SOTA model by Matthew Ballard.

[Shreyas Srinivas]

question : Does Pass@32 mean you collected the best of 32 attempts for each theorem?

[Anh Nguyễn]

Shreyas Srinivas said:

question : Does Pass@32 mean you collected the best of 32 attempts for each theorem?

I think it is more like generating 32 attempts and see if any one of them pass

[Jeremy Tan]

I'm trying to run Goedel-Prover-V2 on my laptop (with no GPU) and I'm always getting the error

SafetensorError: File does not contain tensor model.layers.19.input_layernorm.weight

(or similar). How do I fix this?

I want to see whether the new model can prove IMO 1997 Q3 (#27159), which is not in the training dataset, and if so what the generated output is

[Jeremy Tan]

I've tried it on Colab and I get the same error

[Gavin Zhao]

This looks very promising! I'm particularly curious about the "Verifier-Guided Self-Correction" part and what this means about using this model most effectively. For example, the way I tell Claude Code to write Lean code is:

1. Write some Lean code.
2. Run the Lean compiler to make sure it compiles.
3. If it doesn't compile, read the error message (including context and goal) and come up with a fix. Go back to step 2.

Is Goedel optimized to be used in a similar way? Or are you just doing this feedback loop in training?

[Kaiyu Yang]

Jeremy Tan said:

I'm trying to run Goedel-Prover-V2 on my laptop (with no GPU) and I'm always getting the error

SafetensorError: File does not contain tensor model.layers.19.input_layernorm.weight

(or similar). How do I fix this?

I want to see whether the new model can prove IMO 1997 Q3 (#27159), which is not in the training dataset, and if so what the generated output is

Can you provide the exact steps to reproduce the error (including code and commands you run)?

[Kaiyu Yang]

Gavin Zhao said:

This looks very promising! I'm particularly curious about the "Verifier-Guided Self-Correction" part and what this means about using this model most effectively. For example, the way I tell Claude Code to write Lean code is:

1. Write some Lean code.
2. Run the Lean compiler to make sure it compiles.
3. If it doesn't compile, read the error message (including context and goal) and come up with a fix. Go back to step 2.

Is Goedel optimized to be used in a similar way? Or are you just doing this feedback loop in training?

Something like that at a high level (only in inference). More details will be available in the paper to be released.

[Jeremy Tan]

Kaiyu Yang said:

Can you provide the exact steps to reproduce the error (including code and commands you run)?

1. mkdir goedel; cd goedel in any convenient location.
2. python3 -m venv .venv to create the virtual environment, then source .venv/bin/activate to activate it.
3. python3 -m pip install transformers torch accelerate to install the dependencies
4. For now I am just using the sample script provided on the HuggingFace page as a sanity check. Copy that script and paste it as prover.py in goedel.
5. Run the script – it takes quite a while to download the tensors (naturally), and then at the line

outputs = model.generate(inputs, max_new_tokens=32768)

the error I mentioned is thrown.

[Shreyas Srinivas]

Anh Nguyễn said:

Shreyas Srinivas said:

question : Does Pass@32 mean you collected the best of 32 attempts for each theorem?

I think it is more like generating 32 attempts and see if any one of them pass

So in principle it is possible that the model succeeds on problem X in round n and not in round (n + 1), but it would still count as a success in the statistics right?

[Shreyas Srinivas]

Are these passes parallel or sequential?

[Ping J]

this model sent a shiver down my spine

[Ping J]

never felt this way since gpt4

[Ping J]

Shreyas Srinivas said:

Are these passes parallel or sequential?

i guess parallel, where each containing 3 self-correct iterations

[Bas Spitters]

Is self-correction the same is Proof repair(the Curry-Howard equivalent of Program repair)?
E.g. the work by Talia Ringer https://homes.cs.washington.edu/~djg/theses/ringer_dissertation.pdf

[(deleted)]

The model doesn't always have an accurate model of how Lean works. When Lean provides the compiler errors the model can then fix the code.

[Shange Tang]

Shreyas Srinivas said:

question : Does Pass@32 mean you collected the best of 32 attempts for each theorem?

Pass@32 means that the prover tries 32 times for a theorem, and as long as one is verified by lean then we count it as correct.

[Shange Tang]

Your full name said:

Shreyas Srinivas said:

Are these passes parallel or sequential?

i guess parallel, where each containing 3 self-correct iterations

Yes, our model do the passes in parallel. And each pass contains an initial attempt of writing the entire proof + two rounds of self correction given the lean feedback. The process ended when a correct proof is found at any stage (or two rounds of self corrections still fail to find the proof)

[Bohan Lyu]

Hi! Our inference framework supports multiple rounds of modification and allows for multiple corrections for a single error.
When we report "pass@32 with self-correction," it means that we first perform inference 32 times. If none of the outputs are correct, we then apply a single correction to each error individually. If there are still no correct outputs, we continue from the previous attempts and apply another round of corrections. All of this is done within a 40k context length, which means that some errors cannot be sequentially corrected twice.

[(deleted)]

What Lean and mathlib version is this trained on?

[(deleted)]

I plan to run this model

[Ping J]

i thought this takes the cake until i saw https://deepmind.google/discover/blog/advanced-version-of-gemini-with-deep-think-officially-achieves-gold-medal-standard-at-the-international-mathematical-olympiad/ ... i wonder what post-AGI society will be like... i don't want to live on mars....

[(deleted)]

While a pro-AI person, I don't think speculating about a post-AGI society is very welcome on this Zulip instance

[(deleted)]

Especially when it's off topic for this thread

[Ping J]

i just noticed https://www.gemini.com/ is not owned by Google lol. (i know completely off topic but where else can community members chitchat w

[Kevin Buzzard]

Please take chitchat to the Lean Discord https://discord.com/invite/WZ9bs9UCvx

[Kaiyu Yang]

Jeremy Tan said:

Kaiyu Yang said:

Can you provide the exact steps to reproduce the error (including code and commands you run)?

1. mkdir goedel; cd goedel in any convenient location.
2. python3 -m venv .venv to create the virtual environment, then source .venv/bin/activate to activate it.
3. python3 -m pip install transformers torch accelerate to install the dependencies
4. For now I am just using the sample script provided on the HuggingFace page as a sanity check. Copy that script and paste it as prover.py in goedel.
5. Run the script – it takes quite a while to download the tensors (naturally), and then at the line

outputs = model.generate(inputs, max_new_tokens=32768)

the error I mentioned is thrown.

@Jeremy Tan We just released a GitHub repo (https://github.com/Goedel-LM/Goedel-Prover-V2), and the best way to get help is opening an issue there.

[(deleted)]

Ok. Looks like all Chinese firms use this exact ancient Lean and Mathlib version.

[(deleted)]

I'm also working for a Chinese firm too, so that's... compatibility!

[(deleted)]

Any chance this model gets supported by inference providers in the future?

[(deleted)]

Oh I'm not seeing a recommended prompt

[(deleted)]

Found the prompt. https://github.com/Goedel-LM/Goedel-Prover-V2/blob/main/src/utils.py#L339

[(deleted)]

To line 377.

[(deleted)]

I hope RL doesn't remove its ability to follow human provided proof sketches

[Gavin Zhao]

Wonder how much time/money it would take to re-train models like this with more recent Lean+Mathlib versions :eyes:

[Pawan sasanka ammanamanchi]

The paper seems to have been released here: https://arxiv.org/abs/2508.03613

[(deleted)]

Hello. I used Goedel Prover v2 to prove theorems in this list: https://leanprover.zulipchat.com/#narrow/channel/219941-Machine-Learning-for-Theorem-Proving/topic/AlphaGeometry.20doesn't.20have.20a.20secure.20foundation/near/532238675

I found that even when the theorem statements are expanded into real numbers, Goedel Prover v2 still struggles with them, except the easiest theorems.

I used ollama on Google Colab to run this model: https://ollama.com/alessandrorumampuk/Goedel-Prover-V2:32b

It could be possible that the version on ollama is not optimized, but I found that even when running the official inference code, the performance on my set of theorems is still poor.

Therefore, I believe that good benchmarking could be important in making strong AI models. I feel MiniF2F performance isn't representative of the model's strength in other high school math problems.

[(deleted)]

Screenshot_20250830_182202_com_android_chrome_SameTaskWebApkActivity.jpg

Very disastrous looping behavior here.

[Kelly Davis]

Huỳnh Trần Khanh said:

I found that even when the theorem statements are expanded into real numbers, Goedel Prover v2 still struggles with them...

Which theorems, as stated in PastedText.txt, failed?

[(deleted)]

Many. But try u31 first. Goedel Prover v2 fails on u31.

[(deleted)]

In fact, Goedel Prover v2 rarely succeeds.

[(deleted)]

Thank you for looking into this.

[Alessandro Sosso]

@Yong Lin Hi! Do you have any infomation on how long it took your models to generate a proof on average (both 8B and 32B)?
I am looking for a baseline to compare with my setup

[Bas Spitters]

@Yong Lin @Yong Lin Thanks for the nice work on Goedel. Are there plans on supporting recent versions of lean ?