attempts to improve mcp

app.py

@@ -139,7 +139,7 @@ def chat_handler(
     chat_history: list = None
 ):
     """
-    Handles a single chat interaction with the Kimina Prover model designed for competition-style problem solving and rigorous formal reasoning, achieving state-of-the-art results on the miniF2F benchmark. It supports long context windows (up to 32K tokens) and is capable of both formal and informal mathematical reasoning. This function manages prompt construction, model inference, and output formatting for the Gradio interface, enabling interactive theorem proving and mathematical problem solving.
+    Handles a single chat interaction with the Kimina Prover model designed for competition-style problem solving it is capable of both formal and informal mathematical reasoning and problem solving.
 
     Args:
         user_message (str): The user's input message or formal statement to be solved or discussed by the model. This can be a Lean 4 goal, theorem, or mathematical problem statement.
@@ -156,13 +156,14 @@ def chat_handler(
         )
 
     Example:
-        >> user_message = "Goal:\n  X : UU\n  Y : UU\n  P : UU\n  xp : (X → P) → P\n  yp : (Y → P) → P\n  X0 : X × Y → P\n  x : X\n  ============================\n   (Y → P)"
-        >> informal_prefix = "/-Explain using mathematics-/\n"
-        >> max_tokens = 1234
-        >> chat_history = None
-        >> display_history, output_data_json, code, chat_history = chat_handler(user_message, informal_prefix, max_tokens, chat_history)
+        >>> user_message = "Goal:\n  X : UU\n  Y : UU\n  P : UU\n  xp : (X → P) → P\n  yp : (Y → P) → P\n  X0 : X × Y → P\n  x : X\n  ============================\n   (Y → P)"
+        >>> informal_prefix = "/-Explain using mathematics-/\n"
+        >>> max_tokens = 1234
+        >>> chat_history = None
+        >>> display_history, output_data_json, code, chat_history = chat_handler(user_message, informal_prefix, max_tokens, chat_history)
         # display_history contains the chat turns, output_data_json contains the full model output, code contains extracted Lean4 code.
     """
+    
     if not chat_history or len(chat_history) < 2:
         chat_history = init_chat(user_message, informal_prefix)
         display_history = [("user", user_message)]