polish UI

app.py

@@ -103,7 +103,6 @@ lean_examples = load_lean_examples()
 
 def check_server_health():
     try:
-        # Try to check server status using client
         test_code = "#check Nat"
         responses = client.check(snips=[test_code], show_progress=False)
         return responses.results[0].analyze().status == "valid"
@@ -149,7 +148,27 @@ def create_demo():
     thread.start()
 
     with gr.Blocks(title="Kimina Lean Server") as demo:
-        gr.Markdown("# ⚡ Kimina Lean Server\nOnline Lean 4 Code Verification")
+        gr.Markdown("# 💻 Kimina Lean Server\nOnline Lean 4 Code Verification")
+
+        # README content section
+        with gr.Accordion("📖 About & Features", open=False):
+            gr.Markdown("""
+            ## Overview
+
+            This application provides a user-friendly interface to test and validate formal mathematical proofs written in Lean 4.
+
+            ## Features
+
+            - **Online Lean 4 Code Verification**: Real-time validation of Lean 4 code using an online-deployed [Kimina-Lean-Server](https://github.com/project-numina/kimina-lean-server)
+            - **MiniF2F Example Library**: Browse and load 207 MiniF2F test cases solved by [LongCat-Flash-Thinking](https://github.com/meituan-longcat/LongCat-Flash-Thinking)
+
+            ## Usage Guide
+
+            1. **Write or Select Code**: Either write your own Lean 4 code in the left panel or select from the example library
+            2. **Verify**: Click the "Verify Code" button to check your code against the Kimina server
+            3. **Review Results**: View detailed verification results including any errors or successful validation in the right panel
+            4. **Browse Examples**: Use the pagination controls at the bottom to navigate through the MiniF2F example collection
+            """)
 
         with gr.Row():
             with gr.Column(scale=3):