Lean-focused theorem proving
The publisher describes the series as an open-source model line for automated formal proof generation with Lean compiler feedback.
Open Source Model Profile · Goedel-LM
Goedel-Prover-V2-32B
Goedel-Prover-V2-32B is a 32.76B-parameter Qwen3 text-generation fine-tune from Goedel-LM. Its card presents it as a Lean-focused theorem prover with publisher-reported MiniF2F and PutnamBench results.
- Publisher
- Goedel-LM
- Task
- text-generation
- Model type
- qwen3
- License
- apache-2.0
- Library
- transformers
- Publication status
- Accepted · not indexed
Model overview
The model is published by Goedel-LM as a text-generation fine-tune for automated formal proof generation. The captured configuration identifies Qwen3ForCausalLM with a qwen3 model type, and Safetensors metadata reports 32,762,123,264 parameters. According to the model card, it builds on Qwen/Qwen3-32B with scaffolded data synthesis, verifier-guided self-correction using Lean compiler feedback, and checkpoint averaging.
Recorded capabilities
Publisher-reported MiniF2F results
According to the model card, the 32B model reaches 88.0% on MiniF2F at Pass@32 in standard mode and 90.4% in self-correction mode.
Self-correction procedure
According to the card, self-correction mode generates an initial proof and then performs two revision rounds guided by Lean feedback.
Qwen3 32.76B configuration
Captured config identifies Qwen3ForCausalLM and qwen3, with Safetensors metadata reporting 32,762,123,264 parameters.
Qwen3-32B base lineage
Hub tags identify Qwen/Qwen3-32B as the base model and finetune source.
Use cases in the source record
- Lean 4 proof-generation workflows that follow the card's documented prompt pattern of a proof plan followed by formal code.
- Self-correction experiments where Lean compiler feedback iteratively revises an initial proof candidate, as described by the publisher.
- Theorem-proving benchmark research against the publisher's reported MiniF2F, PutnamBench, and MathOlympiadBench setups.
Limitations and unknowns
- No Ethen-measured evaluation results were extracted; MiniF2F and PutnamBench figures are publisher claims and were not independently verified by Ethen.
- No context-window value, hardware requirement, or training-compute detail was extracted beyond the card's 32K-to-40K token note.
- Comparative claims against other provers come from the publisher and should be read as reported results, not Ethen-verified rankings.
- Provider state is historical snapshot data, not independently refreshed current availability.
Source and provenance
Source: Goedel-LM/Goedel-Prover-V2-32B
Captured: Unknown. Processed: 2026-09-07T19:35:39.638847+00:00.
Goedel-Prover-V2: The Strongest Open-Source Theorem Prover to Date 1. Introduction We introduce Goedel-Prover-V2, an open-source language model series that sets a new state-of-the-art in automated formal proof generation. Built on the standard expert iteration and reinforcement learning pipeline, our approach incorporates three key innovations: (1) Scaffolded data synthesis : We generate synthetic proof tasks of increasing difficulty to progressively train the model, enabling it to master increasingly complex theorems; (2) Verifier-guided self-correction : The model learns to iteratively revise its own proofs by leveraging feedback…
F001F002F003F004F005F006F007F009F010F011F012F013F014F015F016F018F019F020F021