avoids timeout error by reducing the output tokens for unimath examples

app.py

@@ -89,11 +89,10 @@ unimath4 = """Goal:
 additional_info_prompt = "/-Explain using mathematics-/\n"
 
 examples = [
-    [unimath1, additional_info_prompt, 2500],
-    [unimath2, additional_info_prompt, 2500],
-    [unimath3, additional_info_prompt, 2500],
-    [unimath4, additional_info_prompt, 2500],
-    # New examples
+    [unimath1, additional_info_prompt, 1234],
+    [unimath2, additional_info_prompt, 1234],
+    [unimath3, additional_info_prompt, 1234],
+    [unimath4, additional_info_prompt, 1234],
     [
         '''import Mathlib\nimport Aesop\n\nset_option maxHeartbeats 0\n\nopen BigOperators Real Nat Topology Rat\n\n/-- Let $a_1, a_2,\cdots, a_n$ be real constants, $x$ a real variable, and $f(x)=\\cos(a_1+x)+\\frac{1}{2}\\cos(a_2+x)+\\frac{1}{4}\\cos(a_3+x)+\\cdots+\\frac{1}{2^{n-1}}\\cos(a_n+x).$ Given that $f(x_1)=f(x_2)=0,$ prove that $x_2-x_1=m\\pi$ for some integer $m.$-/\ntheorem imo_1969_p2 (m n : \\R) (k : \\N) (a : \\N \\rightarrow \\R) (y : \\R \\rightarrow \\R) (h₀ : 0 < k)\n(h₁ : \\forall x, y x = \\sum i in Finset.range k, Real.cos (a i + x) / 2 ^ i) (h₂ : y m = 0)\n(h₃ : y n = 0) : \\exists t : \\Z, m - n = t * Real.pi := by''',
         "/-- Let $a_1, a_2,\\cdots, a_n$ be real constants, $x$ a real variable, and $f(x)=\\cos(a_1+x)+\\frac{1}{2}\\cos(a_2+x)+\\frac{1}{4}\\cos(a_3+x)+\\cdots+\\frac{1}{2^{n-1}}\\cos(a_n+x).$ Given that $f(x_1)=f(x_2)=0,$ prove that $x_2-x_1=m\\pi$ for some integer $m.$-/",