Fix startup compatibility: Lean output textbox + launch css

app.py

@@ -445,7 +445,7 @@ def analyze_conjecture(
     )
 
 
-with gr.Blocks(title="Conjecture Lean+AI Lab", css=UI_CSS) as demo:
+with gr.Blocks(title="Conjecture Lean+AI Lab") as demo:
     gr.HTML(
         """
         <section class="hero">
@@ -504,7 +504,7 @@ with gr.Blocks(title="Conjecture Lean+AI Lab", css=UI_CSS) as demo:
     )
     work_log_box = gr.Textbox(label="Work Log (always visible)", lines=18, max_lines=30, interactive=False)
     prompt_box = gr.Textbox(label="Prompt Sent to Model", lines=14, max_lines=22, interactive=False)
-    lean_box = gr.Code(label="Lean Verification Stub", language="lean")
+    lean_box = gr.Textbox(label="Lean Verification Stub", lines=12, max_lines=22, interactive=False)
 
     run_btn.click(
         fn=analyze_conjecture,
@@ -528,4 +528,4 @@ demo.queue(default_concurrency_limit=2)
 
 
 if __name__ == "__main__":
-    demo.launch()
+    demo.launch(css=UI_CSS)