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

Gobble-Prover-1.7B

Anonymous model release for peer review.

Gobble-Prover-1.7B is fine-tuned from AI-MO/Kimina-Prover-Distill-1.7B using supervised fine-tuning followed by GRPO. It generates Lean 4 proofs for statements with multiple candidate answers.

This repository contains the model weights, model configuration, and tokenizer. Generated proofs must be checked with Lean.

The base model was developed by Project Numina and Kimi teams and is released under the Apache 2.0 license. See the linked base model card for upstream information.