Upload 3 files

README.md

@@ -1,12 +1,13 @@
----
-title: Testpipeline
-emoji: 👀
-colorFrom: blue
-colorTo: pink
-sdk: gradio
-sdk_version: 5.7.0
-app_file: app.py
-pinned: false
----
-
-Check out the configuration reference at https://huggingface.co/docs/hub/spaces-config-reference
+---
+title: Demo Prover
+emoji: 🐠
+colorFrom: yellow
+colorTo: yellow
+sdk: gradio
+sdk_version: 5.6.0
+python_version: 3.11
+app_file: app.py
+pinned: false
+license: mit
+short_description: nl -> fl
+---

app.py

@@ -0,0 +1,36 @@
+import os
+import gradio as gr
+from huggingface_hub import login
+from transformers import pipeline
+
+# Load the gated model
+#model_name = "RickyDeSkywalker/TheoremLlama"
+model_name = "unsloth/Llama-3.2-1B-Instruct"
+HF_TOKEN = os.environ.get("HF_TOKEN")
+login(HF_TOKEN)
+
+generator = pipeline('text-generation', model=model_name, token=HF_TOKEN)
+
+# 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']
+
+# Gradio Interface
+title = "Lean 4 Code Generation with TheoremLlama"
+description = "Enter a natural language prompt to generate Lean 4 code."
+
+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
+)
+
+# Launch the Gradio app
+interface.launch(ssr_mode=False)

requirements.txt

@@ -0,0 +1 @@
+huggingface_hub