Update README.md

README.md

@@ -4,6 +4,12 @@ base_model:
 - Qwen/Qwen3-32B
 ---
 
+This is the formalizer for tranlating 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
 import torch