Add GitHub repository link to model card

This PR improves the model card by explicitly adding a link to the GitHub repository of the BFS-Prover project (`https://github.com/bytedance-research/BFS-Prover`). This was inferred from the abstract stating the model is open-sourced and the common naming convention of the model's Hugging Face ID. The current card only links to a related library, so this addition will make the project's main codebase more accessible to users. A GitHub badge is also added to the header, and emojis for the paper and code links are updated for better visual clarity.

README.md

@@ -1,15 +1,15 @@
 ---
-license: apache-2.0
+base_model:
+- Qwen/Qwen2.5-Math-7B
 datasets:
 - internlm/Lean-Workbook
 - internlm/Lean-Github
 - AI-MO/NuminaMath-CoT
 language:
 - en
-base_model:
-- Qwen/Qwen2.5-Math-7B
-pipeline_tag: text-generation
 library_name: transformers
+license: apache-2.0
+pipeline_tag: text-generation
 tags:
 - lean4
 - theorem-proving
@@ -20,6 +20,7 @@ tags:
   <h1 style="font-size: 2.0em;">🚀 BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Proving</h1>
   <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://github.com/bytedance-research/BFS-Prover"><img src="https://img.shields.io/badge/GitHub-Code-blue.svg?logo=github" alt="GitHub Code"></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>
@@ -28,8 +29,9 @@ tags:
 
 This repository contains the latest tactic generator model checkpoint from BFS-Prover, a state-of-the-art theorem proving system in Lean4. While the full BFS-Prover system integrates multiple components for scalable theorem proving, we are releasing the core tactic generation model here. Given a proof state in Lean4, the model generates a tactic that transforms the current proof state into a new state, progressively working towards completing the proof.
 
-**📄 Paper: [BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Proving](https://arxiv.org/abs/2502.03438)**
+**📑 Paper: [BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Proving](https://arxiv.org/abs/2502.03438)**
 
+**💻 Code: [GitHub Repository](https://github.com/bytedance-research/BFS-Prover)**
 
 ## ✨ Model Details