Update README.md

README.md

@@ -52,8 +52,9 @@ BFS-Prover achieves state-of-the-art performance on the MiniF2F test benchmark.
 - Combined with simpler search method (BFS) rather than MCTS
 
 ## Usage
-The model expects tactic states in the format `"{state}:::"`, where `:::` serves as a special indicator to signal the model to generate a tactic for the given state. 
-The model will echo back the input state followed by the generated tactic.
+- The model expects Lean4 tactic states in the format `"{state}:::"`
+- `:::` serves as a special indicator to signal the model to generate a tactic for the given state. 
+- The model will echo back the input state followed by the generated tactic.
 
 
 ```python