Update app.py

app.py

@@ -1,5 +1,5 @@
 import os
-import streamlit as st
+import gradio as gr
 from huggingface_hub import login
 from transformers import pipeline
 
@@ -10,21 +10,26 @@ login(HF_TOKEN)
 
 generator = pipeline('text-generation', model=model_name, token=HF_TOKEN)
 
-# Streamlit app
-st.title("Lean 4 Code Generation with TheoremLlama")
-st.write("Enter a natural language prompt to generate Lean 4 code.")
+# Function for generating Lean 4 code
+def generate_lean4_code(prompt):
+    result = generator(prompt, max_length=1000, num_return_sequences=1)
+    return result[0]['generated_text']
 
-# Text input for user prompt
-prompt = st.text_area("Prompt", value="Prove that the sum of two even numbers is even.")
+# Gradio Interface
+title = "Lean 4 Code Generation with TheoremLlama"
+description = "Enter a natural language prompt to generate Lean 4 code."
 
-# Generate button
-if st.button("Generate Lean 4 Code"):
-    with st.spinner("Generating Lean 4 code..."):
-        # Generate code based on the prompt
-        result = generator(prompt, max_length=1000, num_return_sequences=1)
-        generated_code = result[0]['generated_text']
-    
-    # Display the generated code
-    st.code(generated_code, language='lean')
+interface = gr.Interface(
+    fn=generate_lean4_code,
+    inputs=gr.Textbox(
+        label="Prompt",
+        placeholder="Prove that the sum of two even numbers is even.",
+        lines=4
+    ),
+    outputs=gr.Code(label="Generated Lean 4 Code", language="lean"),
+    title=title,
+    description=description
+)
 
-st.markdown("Developed by [Your Name]")
+# Launch the Gradio app
+interface.launch()