Update README.md

README.md

@@ -17,11 +17,13 @@ tags:
 ---
 
 <div align="center">
-<h1 style="font-size: 2.0em;">🚀 BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Proving</h1>
-<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">
-<h2>State-of-the-art tactic generation model in Lean4</h2>
+  <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://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>
 
 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 that achieved state-of-the-art performance on formal mathematics tasks. 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.