Update app.py

app.py

@@ -1,5 +1,5 @@
 """
-app.py - nanoGentzen Neurosymbolic Studio (Gradio + ZeroGPU Edition)
+app.py - nanoGentzen Neurosymbolic Studio (Gradio 6.x Edition)
 Coupling Gemma-2-2B generative reasoning with deterministic Gentzen Sequent Calculus (LI & LK).
 """
 
@@ -9,7 +9,6 @@ import time
 from typing import Any, Dict, Generator, List, Optional, Tuple
 
 import gradio as gr
-import torch
 from huggingface_hub import InferenceClient
 from safetensors.torch import load_file
 
@@ -153,7 +152,7 @@ def chat_stream(
     max_tokens: int,
     max_depth: int,
 ) -> Generator[List[Dict[str, str]], None, None]:
-    # 1. Check if user typed a direct formal sequent
+    # 1. Direct formal sequent check
     has_turnstile = bool(re.search(r"(\|-|⟶|⊢)", message))
     if has_turnstile:
         res = prove_comprehensive(message, max_depth=int(max_depth))
@@ -173,7 +172,7 @@ def chat_stream(
         yield history
         return
 
-    # 2. Serverless Inference Generation
+    # 2. Serverless LLM Stream
     client = InferenceClient()
     api_messages = [{"role": "system", "content": SYSTEM_PROMPT}]
     for msg in history:
@@ -243,15 +242,15 @@ custom_css = """
 .proof-display { font-family: 'JetBrains Mono', monospace; font-size: 0.85rem; }
 """
 
-with gr.Blocks(theme=gr.themes.Soft(primary_hue="indigo"), css=custom_css) as demo:
+with gr.Blocks() as demo:
     gr.Markdown("# 🧠 nanoGentzen Neurosymbolic Studio")
     gr.Markdown(
-        "**System 1 (Neural LLM)** generates chain-of-thought traces, while **System 2 (nanoGentzen)** certifies mathematical soundness in < 25 ms[cite: 8, 10]."
+        "**System 1 (Neural LLM)** generates chain-of-thought traces, while **System 2 (nanoGentzen)** certifies mathematical soundness in < 25 ms."
     )
 
     with gr.Tabs():
         with gr.Tab("💬 Neurosymbolic Chat"):
-            chatbot = gr.Chatbot(type="messages", height=520)
+            chatbot = gr.Chatbot(height=520)
             with gr.Row():
                 msg_input = gr.Textbox(
                     placeholder="Enter a logic problem, question, or sequent (e.g., '(P => Q), ~Q |- ~P')...",
@@ -298,7 +297,7 @@ with gr.Blocks(theme=gr.themes.Soft(primary_hue="indigo"), css=custom_css) as de
             ).then(lambda: "", None, msg_input)
 
         with gr.Tab("🔬 Dual-Mode Logic Prover Lab"):
-            gr.Markdown("### Interactive Sequent Verification ($LI$ vs $LK$)[cite: 8, 10]")
+            gr.Markdown("### Interactive Sequent Verification (LI vs LK)")
             with gr.Row():
                 prover_input = gr.Textbox(
                     value="(P => Q), ~Q |- ~P",
@@ -310,11 +309,11 @@ with gr.Blocks(theme=gr.themes.Soft(primary_hue="indigo"), css=custom_css) as de
 
             with gr.Row():
                 with gr.Column():
-                    gr.Markdown("#### 🌿 Intuitionistic Logic (LI)[cite: 8, 10]")
+                    gr.Markdown("#### 🌿 Intuitionistic Logic (LI)")
                     li_status_out = gr.Textbox(label="Status", interactive=False)
                     li_tree_out = gr.Code(label="Derivation Tree", language="markdown")
                 with gr.Column():
-                    gr.Markdown("#### 🏛️ Classical Logic (LK via Glivenko)[cite: 8, 10]")
+                    gr.Markdown("#### 🏛️ Classical Logic (LK via Glivenko)")
                     lk_status_out = gr.Textbox(label="Status", interactive=False)
                     lk_tree_out = gr.Code(label="Derivation Tree", language="markdown")
 
@@ -325,4 +324,4 @@ with gr.Blocks(theme=gr.themes.Soft(primary_hue="indigo"), css=custom_css) as de
             )
 
 if __name__ == "__main__":
-    demo.launch()
+    demo.launch(theme=gr.themes.Soft(primary_hue="indigo"), css=custom_css)