Update app.py

app.py

@@ -148,10 +148,12 @@ Output a rigorous proof or meaningful insight even when a full proof is impossib
 
 iface = gr.Interface(
     fn=theorem_prover, 
-    inputs=gr.Textbox(label="Enter Formula (e.g., x > 5 and y < 10)"), 
-    outputs=gr.Markdown(label="Result"),  # Output as HTML
+    inputs=gr.Textbox(label="Enter the theorem you want to prove or disprove"), 
+    outputs=gr.Markdown(label="Agent's response"),  # Output as HTML
     title="Theorem proving agent",
-    description="Enter a logical formula using Z3 syntax to check its satisfiability."
+    description="Theorem Proving Agent is an AI-powered system that autonomously selects proof strategies and generates formal proofs for mathematical theorems. As part of AI Quotient’s Millennium Math Challenge, it advances automated reasoning to tackle some of the hardest unsolved problems in mathematics.",
+    theme = gr.themes.Ocean(),
+    examples = ["Every prime number greater than 2 is odd.", "The sum of two rational numbers is always rational.", "The power set of any set has strictly greater cardinality than the set itself."]
 )
 
 # Launch the app