EPFL-LARA/lean-world-model-qwen3-8b-reasoning-grpo

TEXT GENERATIONPricing:Input $0.468 / Output $1.82Concurrent Unit Cost:1Model Size:8BQuant:FP8Context Size:32kTool Calling:SupportedPublished:Oct 16, 2026Architecture:Transformer Featherless Exclusive Cold

The EPFL-LARA/lean-world-model-qwen3-8b-reasoning-grpo is an 8 billion parameter Qwen3-based model developed by EPFL-LARA, specifically designed for generating Lean proofs. It incorporates predicted goal states and compiler diagnostics within inline comments and supports repair attempts within a single response. This variant uniquely includes an informal reasoning plan before each proof attempt, making it highly specialized for formal theorem proving in Lean 4.

Loading preview...

Lean World-Model Prover — Qwen3-8B

This model, developed by EPFL-LARA, is an 8 billion parameter Qwen3-based language model specifically engineered for generating formal proofs in Lean 4. It stands out by integrating predicted goal states and compiler diagnostics directly into inline comments, facilitating an iterative proof development process with built-in repair capabilities within a single response. A key differentiator is its ability to generate an informal reasoning plan prior to attempting a formal proof, enhancing its utility for complex theorem proving.

Key Capabilities

  • Lean Proof Generation: Specializes in producing formal proofs for Lean 4, including import Mathlib and theorem definitions.
  • Integrated Diagnostics: Provides predicted goal states and compiler feedback directly within the generated proof comments (/- <feedback> ... </feedback> -/).
  • Reasoning Plan Generation: Creates an informal reasoning plan (including sections like [Problem Restatement], [Useful Observations], [Reasoning Path], [Key Derivation], [Proof Type], [Formal Anchors], and [Final Solution]) before generating the formal Lean code.
  • Proof Repair Mechanism: Supports iterative refinement by generating [Error Analysis], [Revised Reasoning], and [Updated Proof Plan] sections for failed proof attempts, followed by a corrected solution.
  • Context Length: Utilizes a 32,768-token context window for comprehensive problem understanding and proof generation.

Good For

  • Formal Theorem Proving: Ideal for researchers and developers working with Lean 4 who need automated assistance in constructing proofs.
  • Educational Tools: Can serve as a valuable tool for learning formal methods by demonstrating reasoning paths and proof construction.
  • Automated Proof Assistants: Enhances existing proof assistant workflows by providing initial proof attempts and diagnostic feedback.
  • Complex Mathematical Reasoning: Particularly suited for tasks requiring structured, step-by-step logical deduction in a formal system.

Finetunes
1 models