Update README.md

README.md

@@ -3,6 +3,11 @@ license: apache-2.0
 base_model:
 - Qwen/Qwen3-8B
 ---
+This is the formalizer for translating infromal math problem into formal statement in Lean 4. In Goedel-Prover-V2 project we use this formalizer in generating lean4 statements.
+Different from all previous open-source formalizers, this formalizer has the ability to think before generating the lean4 statements, which significantly increases the acurracy of the translation.
+In our internal evaluation, we test the performance of formalizers on a eval set containing 300 informal statements from Omni-MATH. Kimina-formalizer-8B successfully translates 161/300 statements, while Goedel-Formalizer-V2-32B success in 228 statements. 
+
+Here is an example code to use this formalizer:
 
 ```
 from transformers import AutoModelForCausalLM, AutoTokenizer