ByteDance-Seed
/

BFS-Prover-V1-7B

Text Generation

theorem-proving

formal-mathematics

text-generation-inference

Model card Files Files and versions

RanXinByteDance commited on Feb 25, 2025

Commit

e837c70

·

verified ·

1 Parent(s): 12cf310

Update README.md

Files changed (1) hide show

README.md +1 -1

README.md CHANGED Viewed

@@ -21,7 +21,7 @@ tags:
   <div style="display: flex; justify-content: center; gap: 8px; flex-wrap: wrap;">
     <a href="https://arxiv.org/abs/2502.03438"><img src="https://img.shields.io/badge/arXiv-2502.03438-b31b1b.svg" alt="arXiv"></a>
     <a href="https://choosealicense.com/licenses/apache-2.0/"><img src="https://img.shields.io/badge/License-Apache%202.0-blue.svg" alt="License: Apache 2.0"></a>
-    <img src="https://img.shields.io/badge/Lean-4-orange" alt="Lean 4">
   </div>
   <h2>State-of-the-art tactic generation model in Lean4</h2>
 </div>

   <div style="display: flex; justify-content: center; gap: 8px; flex-wrap: wrap;">
     <a href="https://arxiv.org/abs/2502.03438"><img src="https://img.shields.io/badge/arXiv-2502.03438-b31b1b.svg" alt="arXiv"></a>
     <a href="https://choosealicense.com/licenses/apache-2.0/"><img src="https://img.shields.io/badge/License-Apache%202.0-blue.svg" alt="License: Apache 2.0"></a>
+    <a href="https://github.com/leanprover-community/mathlib4"><img src="https://img.shields.io/badge/Lean-4-orange" alt="Lean 4"></a>
   </div>
   <h2>State-of-the-art tactic generation model in Lean4</h2>
 </div>