Goedel-Prover-V2

An open-weight model family for Lean proof generation and self-correction.

• Developer / Organization: Goedel-LM research team
• Category: Proof models & model integrations
• Purpose: Provide open-weight Lean theorem-proving models.
• Key features: Formal proof generation with released model checkpoints, evaluation tools and self-correction workflows.
• Availability: Model / model-integration project; consult model and code licenses separately
• License: Not verified in the linked source (source (opens in a new tab))
• Website / Source code: https://github.com/Goedel-LM/Goedel-Prover-V2 (opens in a new tab)
• Version: Model family: V2 (8B and 32B)
• Version source: Official release or documentation (opens in a new tab)
• Last checked: 2026-11-01