Spaces:

Tonic
/

Math

Running on Zero

Tonic commited on 7 days ago

Commit

447b558

verified ·

1 Parent(s): 0ac9edc

Update app.py

Files changed (1) hide show

app.py CHANGED Viewed

@@ -105,7 +105,7 @@ Join us : 🌟TeamTonic🌟 is always making cool demos! Join our active builder
         fn=solve_math_problem,
         outputs=[
             gr.JSON(label="Full Output"),
-            gr.Code(label="Extracted Lean4 Code", language="plaintext")
         ],
         inputs=[
             gr.Textbox(label="🤔Enter your Lean4 formal statement", lines=7),

         fn=solve_math_problem,
         outputs=[
             gr.JSON(label="Full Output"),
+            gr.Code(label="Extracted Lean4 Code", language="python")
         ],
         inputs=[
             gr.Textbox(label="🤔Enter your Lean4 formal statement", lines=7),