Update README.md

README.md

@@ -15,11 +15,10 @@ import json
 def statement_translation_inference(informal_statement):
     return F"""
 I want you to translate a informal statment to formal statement in  lean 4, the informal statement of the problem is:
-```
+
 {informal_statement}
-```
-The output is 
-```lean
+
+The output is
 """
 
 model_name = "Goedel-LM/Goedel-Formalizer-32B-LeanWorkbookAnnotated"
@@ -35,19 +34,8 @@ sampling_params = SamplingParams(
 )
 
 data_list = [{
-  "informal_statement": "Consider the terms of an arithmetic sequence: $-\frac{1}{3}, y+2, 4y, \ldots$. Solve for $y$.",
-  "informal_proof": """For an arithmetic sequence, the difference between consecutive terms must be equal. Therefore, we can set up the following equations based on the sequence given:
-\[ (y + 2) - \left(-\frac{1}{3}\right) = 4y - (y+2) \]
-
-Simplify and solve these equations:
-\[ y + 2 + \frac{1}{3} = 4y - y - 2 \]
-\[ y + \frac{7}{3} = 3y - 2 \]
-\[ \frac{7}{3} + 2 = 3y - y \]
-\[ \frac{13}{3} = 2y \]
-\[ y = \frac{13}{6} \]
-
-Thus, the value of $y$ that satisfies the given arithmetic sequence is $\boxed{\frac{13}{6}}$.""" 
-}]
+  "informal_statement": "Consider the terms of an arithmetic sequence: $-\frac{1}{3}, y+2, 4y, \ldots$. Solve for $y$."
+  }]
 
 model_inputs = [statement_translation_inference(idata["informal_statement"], idata["informal_proof"]) for idata in data_list]