adds examples

app.py

@@ -93,7 +93,23 @@ examples = [
     [unimath1, additional_info_prompt, 2500],
     [unimath2, additional_info_prompt, 2500],
     [unimath3, additional_info_prompt, 2500],
-    [unimath4, additional_info_prompt, 2500]
+    [unimath4, additional_info_prompt, 2500],
+    # New examples
+    [
+        '''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.$-/",
+        2500
+    ],
+    [
+        '''import Mathlib\nimport Aesop\n\nset_option maxHeartbeats 0\n\nopen BigOperators Real Nat Topology Rat\n\n/-- Suppose that $h(x)=f^{-1}(x)$. If $h(2)=10$, $h(10)=1$ and $h(1)=2$, what is $f(f(10))$? Show that it is 1.-/\ntheorem mathd_algebra_209 (σ : Equiv \\R \\R) (h₀ : σ.2 2 = 10) (h₁ : σ.2 10 = 1) (h₂ : σ.2 1 = 2) :\nσ.1 (σ.1 10) = 1 := by''',
+        "/-- Suppose that $h(x)=f^{-1}(x)$. If $h(2)=10$, $h(10)=1$ and $h(1)=2$, what is $f(f(10))$? Show that it is 1.-/",
+        2500
+    ],
+    [
+        '''import Mathlib\nimport Aesop\n\nset_option maxHeartbeats 0\n\nopen BigOperators Real Nat Topology Rat\n\n/-- At which point do the lines $s=9-2t$ and $t=3s+1$ intersect? Give your answer as an ordered pair in the form $(s, t).$ Show that it is (1,4).-//\ntheorem mathd_algebra_44 (s t : \\R) (h₀ : s = 9 - 2 * t) (h₁ : t = 3 * s + 1) : s = 1 \\wedge t = 4 := by''',
+        "/-- At which point do the lines $s=9-2t$ and $t=3s+1$ intersect? Give your answer as an ordered pair in the form $(s, t).$ Show that it is (1,4).-/",
+        2500
+    ],
 ]
 
 model_name = "AI-MO/Kimina-Prover-Distill-8B"
@@ -176,9 +192,10 @@ def main():
             with gr.Column:
                 gr.Markdown(description)
             with gr.Column:
-                gr.Markdown(joinus)        
+                gr.Markdown(joinus)
         with gr.Row():
             with gr.Column():
+
                 user_input = gr.Textbox(label="Your message or formal statement", lines=4)
                 informal = gr.Textbox(value=additional_info_prompt, label="Optional informal prefix")
                 max_tokens = gr.Slider(minimum=150, maximum=4096, value=2500, label="Max Tokens")
@@ -189,8 +206,12 @@ def main():
                     json_out = gr.JSON(label="Full Output")
                     code_out = gr.Code(label="Extracted Lean4 Code", language="python")
         state = gr.State([])
-        # On submit, call chat_handler
         submit.click(chat_handler, [user_input, informal, max_tokens, state], [chat, json_out, code_out, state])
+        gr.Examples(
+                    examples=examples,
+                    inputs=["user_input", "informal", "max_tokens"],
+                    label="Example Problems"
+                )
         gr.Markdown(citation)
     demo.launch()