Update README.md

README.md

@@ -50,40 +50,3 @@ output = model.generate(text, sampling_params=sampling_params)
 output_text = output[0].outputs[0].text
 print(output_text)
 ```
-
-# Lemmas usage
-
-You can provide lemmas to the model to assist its reasoning, and it uses them as tools to help construct or guide the formal proof of the theorem.
-
-```python
-problem = "What is the smallest positive integer $t$ such that there exist integers $x_{1}, x_{2}, \\ldots, x_{t}$ with $$ x_{1}^{3}+x_{2}^{3}+\\cdots+x_{t}^{3}=2002^{2002} ? $$"
-formal_statement = """import Mathlib
-
-
-lemma lemma_1 (x : ℤ) : x^3 ≡ 0 [ZMOD 9] ∨ x^3 ≡ 1 [ZMOD 9] ∨ x^3 ≡ 8 [ZMOD 9] := by
-  have h1 : x % 9 = 0 ∨ x % 9 = 1 ∨ x % 9 = 2 ∨ x % 9 = 3 ∨ x % 9 = 4 ∨ x % 9 = 5 ∨ x % 9 = 6 ∨ x % 9 = 7 ∨ x % 9 = 8 := by
-    omega
-  rcases h1 with (h1 | h1 | h1 | h1 | h1 | h1 | h1 | h1 | h1) <;> simp [Int.ModEq, pow_three, Int.add_emod, Int.mul_emod, h1, Int.sub_emod]
-
-
-theorem number_theory_25102 :
-    IsLeast {t : ℕ | 0 < t ∧ ∃ x : Fin t → ℤ, ∑ i : Fin t, (x i)^3 = 2002^2002} 4 := by
-
-"""
-prompt = "Think about and solve the following problem step by step in Lean 4."
-prompt += f"\n# Problem:{problem}"""
-prompt += f"\n# Formal statement:\n```lean4\n{formal_statement}\n```\n"
-messages = [
-    {"role": "system", "content": "You are an expert in mathematics and Lean 4."},
-    {"role": "user", "content": prompt}
-]
-text = tokenizer.apply_chat_template(
-    messages,
-    tokenize=False,
-    add_generation_prompt=True
-)
-sampling_params = SamplingParams(temperature=0.6, top_p=0.95, max_tokens=8096)
-output = model.generate(text, sampling_params=sampling_params)
-output_text = output[0].outputs[0].text
-print(output_text)
-```