fixes

app.py

@@ -15,8 +15,7 @@ LEAN4_DEFAULT_HEADER = (
 title = "# 🙋🏻‍♂️Welcome to 🌟Tonic's 🌕💉👨🏻‍🔬Moonshot Math"
 
 description = """
-     **Kimina-Prover-72B** is a state-of-the-art large formal reasoning model for Lean 4, achieving **80%+ pass rate** on the miniF2F benchmark, outperforming all prior works.\
-Trained with Reinforcement Learning, 72B parameters, and a 32K token context window.\
+     **🌕💉👨🏻‍🔬AI-MO/Kimina-Prover-Distill-8B is a theorem proving model developed by Project Numina and Kimi teams, focusing on competition style problem solving capabilities in Lean 4. It is a distillation of AI-MO/Kimina-Prover-72B, a model trained via large scale reinforcement learning. It achieves 77.86% accuracy with Pass@32 on MiniF2F-test.\
 - [Kimina-Prover-Preview GitHub](https://github.com/MoonshotAI/Kimina-Prover-Preview)\
 - [Hugging Face: AI-MO/Kimina-Prover-72B](https://huggingface.co/AI-MO/Kimina-Prover-72B)\
 - [Kimina Prover blog](https://huggingface.co/blog/AI-MO/kimina-prover)\
@@ -195,22 +194,22 @@ def main():
                 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")
+                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")
                 submit = gr.Button("Send")
-                gr.Examples(
-                    examples=examples,
-                    inputs=[user_input, informal, max_tokens],
-                    label="Example Problems"
-                )
             with gr.Column():
-                chat = gr.Chatbot(label="Chat History")
+                chat = gr.Chatbot(label="🌕💉👨🏻‍🔬Kimina Prover 8B")
                 with gr.Accordion("Complete Output", open=False):
                     json_out = gr.JSON(label="Full Output")
                     code_out = gr.Code(label="Extracted Lean4 Code", language="python")
         state = gr.State([])
         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()