anonymous-submission-ICLR2027/Gobble-Prover-1.7B

TEXT GENERATIONPricing:Input $0.32 / Cached $0.064 / Output $1.6Concurrent Unit Cost:1Model Size:2BQuant:BF16Context Size:32kTool Calling:SupportedPublished:Sep 18, 2026License:apache-2.0Architecture:Transformer Open Weights Featherless Exclusive Cold

Gobble-Prover-1.7B is a 2 billion parameter language model, fine-tuned from AI-MO/Kimina-Prover-Distill-1.7B, specifically designed for generating Lean 4 proofs. Utilizing supervised fine-tuning and GRPO, it excels at producing proofs for mathematical statements with multiple candidate solutions. This model is optimized for automated theorem proving within the Lean 4 ecosystem, offering a specialized tool for formal verification tasks.

Loading preview...

Gobble-Prover-1.7B: Specialized Lean 4 Proof Generation

Gobble-Prover-1.7B is a 2 billion parameter model developed for the specialized task of generating formal proofs in Lean 4. It is fine-tuned from the AI-MO/Kimina-Prover-Distill-1.7B base model, leveraging supervised fine-tuning followed by GRPO (Goal-oriented Reinforcement Learning for Proof Optimization).

Key Capabilities

  • Lean 4 Proof Generation: Primarily focused on producing valid Lean 4 proofs.
  • Multi-Candidate Statement Proving: Designed to handle mathematical statements that may have several potential proof paths or solutions.
  • Formal Verification: Provides a tool for automating aspects of formal verification within the Lean 4 theorem prover.

Good For

  • Automated Theorem Proving: Ideal for researchers and developers working on automating proof generation in Lean 4.
  • Formal Mathematics: Useful for assisting with the formalization of mathematical theories and proofs.
  • Educational Tools: Can be integrated into systems for teaching or exploring formal logic and proof construction in Lean 4.

Users should note that generated proofs require external checking with Lean to ensure correctness.

Finetunes
1 models