adds usage example

app.py

@@ -132,7 +132,39 @@ def init_chat(formal_statement, informal_prefix):
     ]
 
 @spaces.GPU
-def chat_handler(user_message, informal_prefix, max_tokens, chat_history):
+def chat_handler(
+    user_message: str,
+    informal_prefix: str = "/-Explain using mathematics-/\n",
+    max_tokens: int = 2500,
+    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.
+
+    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.
+        informal_prefix (str, optional): An optional informal explanation or context to prepend to the formal statement. Defaults to '/-Explain using mathematics-/\n'.
+        max_tokens (int, optional): The maximum number of tokens to generate in the model's response. Must be between 150 and 4096. Defaults to 2500.
+        chat_history (list, optional): The conversation history as a list of message dicts, each with 'role' and 'content'. Used to maintain context across turns. Defaults to None.
+
+    Returns:
+        tuple: (
+            display_history (list of tuples): List of (role, content) pairs for display in the chat UI.
+            output_data_json (str): JSON string containing model input, output, extracted Lean4 code, and updated chat history.
+            code (str): Extracted Lean4 code from the model's response, if present.
+            chat_history (list): Updated chat history including the latest user and assistant messages.
+        )
+
+    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)
+        # 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)]