attempts to improve mcp

app.py

@@ -139,9 +139,7 @@ def chat_handler(
     chat_history: list = None
 ):
     """
-    Handles a single chat interaction with the Kimina Prover model, a state-of-the-art large language model for formal mathematical theorem proving in Lean 4, developed by Project Numina and the Kimi teams [[Kimina-Prover-Preview]](https://github.com/MoonshotAI/Kimina-Prover-Preview/tree/master).
-
-    The Kimina Prover model is 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 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.
 
     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.