Update README.md

README.md

@@ -7,9 +7,12 @@ license: mit
   <a href="https://goedel-lm.github.io/" target="_blank" style="margin: 2px;">
     <img alt="Homepage" src="https://img.shields.io/badge/%F0%9F%A4%96%20Homepage-Goedel-536af5?color=536af5&logoColor=white" style="display: inline-block; vertical-align: middle;"/>
   </a>
-  <a href="https://huggingface.co/Goedel-LM" target="_blank" style="margin: 2px;">
-    <img alt="Hugging Face" src="https://img.shields.io/badge/%F0%9F%A4%97%20Hugging%20face-Goedel-ffc107?color=ffc107&logoColor=white" style="display: inline-block; vertical-align: middle;"/>
+  <a href="https://github.com/Goedel-LM/Goedel-Prover" target="_blank" style="margin: 2px;">
+    <img alt="Github" src="https://img.shields.io/badge/GitHub-Goedel-blue?style=flat-square&logo=github&logoColor=white" style="display: inline-block; vertical-align: middle;"/>
   </a>
+  <!-- <a href="https://huggingface.co/Goedel-LM" target="_blank" style="margin: 2px;">
+    <img alt="HuggingFace" src="https://img.shields.io/badge/%F0%9F%A4%97%20Hugging%20face-Goedel-ffc107?color=ffc107&logoColor=white" style="display: inline-block; vertical-align: middle;"/>
+  </a> -->
 </div>
 
 <div align="center" style="line-height: 1;">
@@ -41,7 +44,9 @@ license: mit
 
 ## 1. Introduction
 
-Large language models (LLMs) have shown impressive capabilities in reasoning, particularly in solving mathematical problems. However, relying solely on natural language for reasoning poses challenges in verification, undermining trust in practical applications. Formal theorem proving offers a promising solution: training LLMs to generate proofs in formal languages that can be mechanically verified. A key obstacle in this domain is the scarcity of formal data. To address this challenge, we use language models to autoformalize extensive math problems from natural language to formal statements. Next, we train the prover through a standard iterative process that alternates between attempting to prove these statements and training the prover using newly found proofs. Our model outperforms the previous state-of-the-art (SOTA) whole-proof generation model, DeepSeek-Prover-v1.5-RL, by 7.6% on the miniF2F benchmark, achieving a Pass@32 score of 57.6%. Our model successfully solves 7 problems on the challenging PutnamBench by Pass@512, securing the 1st position on the leaderboard. Furthermore, we have cumulatively solved 29.7K problems in Lean Workbook, significantly increasing the 15.7K proofs found by prior methods. We contribute open-source resources to support future research in formal theorem proving.
+Large language models (LLMs) have demonstrated remarkable reasoning capabilities, particularly in solving mathematical problems. There are two main approaches to tackling math problems: the informal approach, which involves reasoning in natural language, and the formal approach, which relies on proof assistants such as Lean and Isabelle that use formal and machine checkable mathematical languages. State-of-the-art reasoning LLMs such as OpenAI o1 and Deepseek R1 excel at informal math but not at formal math. While the informal approach is more intuitive to humans, it also poses significant challenges in proof verification, undermining its reliability in practical applications.
+
+We introduce Goedel-Prover, a state-of-the-art (SOTA) open-source model for formal mathematics that generates machine-verifiable proofs. On the miniF2F benchmark at Pass@32, our model achieves a 57.6% success rate, surpassing the previous SOTA open-source model for whole-proof generation by a significant 7.6% margin. On the challenging PutnamBench, our model successfully solves 7 problems at Pass@512, securing 1st place on the leaderboard. Additionally, we have cumulatively generated 29.7K formal proofs for problems in the Lean Workbook, a substantial increase over the 15.7K proofs produced by prior methods. A key challenge in formal mathematics is data scarcity. To address this, we train LLMs to auto-formalize a large corpus of mathematical problems, converting natural language descriptions into formal statements. We then train a prover through an iterative process, alternating between generating proofs for these formalized statements and refining the model using the newly discovered proofs. Our project contributes to the open-source community for advancing research in formal theorem proving, and developing more capable mathematical reasoning systems.
 
 <p align="center">
   <img width="100%" src="performance.png">
@@ -77,10 +82,10 @@ Large language models (LLMs) have shown impressive capabilities in reasoning, pa
 <div align="center">
 MultiDataset
 
-|                       | miniF2F    | ProofNet   | FormalNumina | Lean-workbook | **Average**   |
-|-----------------------|------------|------------|--------------|---------------|-----------|
-| Deepseek-Prover-v1.5-RL | 50.0%     | **16.0%**  | 54.0%        | 14.7%         | 33.7%     |
-| **Goedel-Prover-SFT**         | **57.6%**  | 15.2%  | **61.2%**  | **21.2%**  | **38.8%**  |
+|                       | miniF2F    | ProofNet   | FormalNumina | Lean-workbook | 
+|-----------------------|------------|------------|--------------|---------------|
+| Deepseek-Prover-v1.5-RL | 50.0%     | **16.0%**  | 54.0%        | 14.7%         |
+| **Goedel-Prover-SFT**         | **57.6%**  | 15.2%  | **61.2%**  | **21.2%**  | 
 </div>
 
 **Caption:** Comparison of Goedel-Prover-SFT with Deepseek-Prover-v1.5-RL for whole proof generation on miniF2F, ProofNet,FormalNumina,Lean-workbook. We report the Pass@32 performance for miniF2F, ProofNet, and FormalNumina datasets. For the Lean-workbook, we evaluate performance using Pass@16 due to the large number of problems (140K) it contains, allowing us to save on computational costs. FormalNumina is a private test set created by formalizing a randomly sampled collection of 250 problems from Numina.
@@ -90,18 +95,29 @@ Putnam
   
 | Ranking | Model                                                 | Type                  | Num-solved | Compute            |
 |---------|-------------------------------------------------------|-----------------------|------------|---------------------|
-| 1       | **Goedel-Prover-SFT** 💚                                   | Whole Proof Generation | 7          | 512                 |
+| 1       | **Goedel-Prover-SFT** 🟩      | Whole Proof Generation | 7          | 512                 |
 | 1       | ABEL                                           | Tree Search Method     | 7          | 596                 |
-| 3       | **Goedel-Prover-SFT** 💚                                   | Whole Proof Generation | 6          | 32                  |
-| 3       | InternLM2.5-StepProver  💚                      | Tree Search Method     | 6          | 2×32×600            |
-| 5       | InternLM 7B  💚                                  | Whole Proof Generation | 4          | 4096                |
+| 3       | **Goedel-Prover-SFT** 🟩                                   | Whole Proof Generation | 6          | 32                  |
+| 3       | InternLM2.5-StepProver  🟩                       | Tree Search Method     | 6          | 2×32×600            |
+| 5       | InternLM 7B                                    | Whole Proof Generation | 4          | 4096                |
 | 6       | GPT-4o                                        | Whole Proof Generation | 1          | 10                  |
-| 7       | COPRA (GPT-4o) 💚                                | Whole Proof Generation | 1          | 1                   |
-| 8       | ReProver w/ retrieval  💚                        | Whole Proof Generation | 0          | 1                   |
-| 9       | ReProver w/o retrieval  💚                       | Whole Proof Generation | 0          | 1                   |  
+| 7       | COPRA (GPT-4o) 🟩                                | Whole Proof Generation | 1          | 1                   |
+| 8       | ReProver w/ retrieval  🟩                         | Whole Proof Generation | 0          | 1                   |
+| 9       | ReProver w/o retrieval  🟩                        | Whole Proof Generation | 0          | 1                   |  
 </div>
 
-**Caption:** Our model rank the 1st on [Putnam Leaderboard](https://trishullab.github.io/PutnamBench/leaderboard.html). The performance numbers for existing works are taken from the leaderboard. 💚 indicates open sourced models.
+**Caption:** Our model rank the 1st on [Putnam Leaderboard](https://trishullab.github.io/PutnamBench/leaderboard.html). The performance numbers for existing works are taken from the leaderboard. 🟩  indicates open sourced models.
+
+## 3. Dataset Downloads
+
+We are also releasing 29,7K proofs of the problems in Lean-workbook found by our Goedel-Prover-SFT.
+
+<div align="center">
+
+|            **Datasets**            |                          **Download**                         |
+| :-----------------------------: | :----------------------------------------------------------: |
+|   Lean-workbook-proofs   | [🤗 HuggingFace](https://huggingface.co/datasets/Goedel-LM/Lean-workbook-proofs) |
+</div>
 
 ## 4. Citation
 ```latex