Add Hugging Face Spaces deployment with Groq API

- Replace Ollama/local LLM with Groq API (langchain-groq + groq SDK)
- Default model changed to llama-3.3-70b-versatile across all LLM clients
- Add Gradio web UI (app.py) as the HF Spaces entry point
- Add Dockerfile with Ubuntu 22.04 + Lean 4 via elan, Mathlib pre-warmed
- Update requirements.txt: remove ollama/langchain-ollama, add groq/langchain-groq/gradio

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

Dockerfile

@@ -0,0 +1,41 @@
+FROM ubuntu:22.04
+
+ENV DEBIAN_FRONTEND=noninteractive
+ENV LANG=C.UTF-8
+
+RUN apt-get update && apt-get install -y \
+    python3.11 python3-pip python3.11-dev \
+    curl git build-essential \
+    && rm -rf /var/lib/apt/lists/*
+
+# Install elan (Lean version manager) and the stable Lean 4 toolchain
+RUN curl -sSf https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh \
+    | sh -s -- -y --no-modify-path --default-toolchain leanprover/lean4:stable
+ENV PATH="/root/.elan/bin:$PATH"
+
+# Confirm lean is available
+RUN lean --version
+
+WORKDIR /app
+
+# Install Python deps first (layer-cached separately from source)
+COPY requirements.txt .
+RUN pip3 install --no-cache-dir -r requirements.txt
+
+COPY . .
+
+# Pre-warm the Lean + Mathlib environment so the first user request isn't slow.
+# This runs lean_interact with Mathlib once during the Docker build, triggering
+# Mathlib cache population. Failures are tolerated so the image still builds.
+RUN python3 -c "
+import sys; sys.path.insert(0, '/app/src')
+from lean_verifier import LeanEnvironment
+env = LeanEnvironment(use_mathlib=True)
+env.verify_proof('import Mathlib\n\n#check Nat.add_comm')
+env.close()
+" || echo "Lean warm-up skipped (non-fatal)"
+
+EXPOSE 7860
+ENV GRADIO_SERVER_NAME=0.0.0.0
+
+CMD ["python3", "app.py"]

app.py

@@ -0,0 +1,108 @@
+import io
+import os
+import sys
+import tempfile
+from contextlib import redirect_stdout
+
+import gradio as gr
+
+sys.path.insert(0, os.path.join(os.path.dirname(__file__), "src"))
+
+from langgraph_agent import LangGraphAgent
+
+GROQ_MODELS = [
+    "llama-3.3-70b-versatile",
+    "deepseek-r1-distill-llama-70b",
+    "gemma2-9b-it",
+    "llama-3.1-8b-instant",
+]
+
+EXAMPLE_CODE = """\
+import Mathlib
+
+theorem add_zero_simple (n : ℕ) : n + 0 = n := by
+  sorry
+"""
+
+
+def solve_proof(lean_code: str, model_name: str, max_retries: int) -> tuple[str, str, str]:
+    if not lean_code.strip():
+        return "Please enter some Lean 4 code.", "", ""
+
+    if not os.environ.get("GROQ_API_KEY"):
+        return "GROQ_API_KEY is not set. Add it as a Space secret.", "", ""
+
+    tmp = tempfile.NamedTemporaryFile(suffix=".lean", mode="w", delete=False, dir="/tmp")
+    try:
+        tmp.write(lean_code)
+        tmp.close()
+
+        log_buf = io.StringIO()
+        with redirect_stdout(log_buf):
+            agent = LangGraphAgent(model_name=model_name, max_retries=int(max_retries))
+            result = agent.solve_file_detailed(tmp.name)
+
+        with open(tmp.name) as f:
+            final_code = f.read()
+
+        logs = log_buf.getvalue()
+
+        if result["success"]:
+            status = f"Proof verified on attempt {result['solved_at_attempt']} of {result['total_attempts']}."
+        else:
+            status = f"Could not find a proof after {result['total_attempts']} attempts."
+
+        return status, final_code, logs
+
+    except Exception as exc:
+        return f"Error: {exc}", "", ""
+    finally:
+        os.unlink(tmp.name)
+
+
+with gr.Blocks(title="Lean 4 Proof Assistant") as demo:
+    gr.Markdown(
+        "# Lean 4 Proof Assistant\n"
+        "Paste Lean 4 code containing `sorry` placeholders. "
+        "The agent will use Mathlib RAG + an LLM to complete the proof and verify it with the Lean REPL.\n\n"
+        "> **Note:** Proof attempts can take 1–5 minutes. Please be patient."
+    )
+
+    with gr.Row():
+        with gr.Column(scale=1):
+            lean_input = gr.Code(
+                label="Lean 4 Code",
+                language=None,
+                value=EXAMPLE_CODE,
+                lines=18,
+            )
+            with gr.Row():
+                model_dropdown = gr.Dropdown(
+                    choices=GROQ_MODELS,
+                    value=GROQ_MODELS[0],
+                    label="Model",
+                )
+                retries_slider = gr.Slider(
+                    minimum=1, maximum=10, value=5, step=1,
+                    label="Max Retries",
+                )
+            submit_btn = gr.Button("Solve Proof", variant="primary")
+
+        with gr.Column(scale=1):
+            status_output = gr.Textbox(label="Status", interactive=False, lines=2)
+            code_output = gr.Code(
+                label="Completed Proof",
+                language=None,
+                interactive=False,
+                lines=14,
+            )
+            logs_output = gr.Textbox(label="Agent Logs", interactive=False, lines=8)
+
+    submit_btn.click(
+        solve_proof,
+        inputs=[lean_input, model_dropdown, retries_slider],
+        outputs=[status_output, code_output, logs_output],
+    )
+
+if __name__ == "__main__":
+    demo.launch(server_name="0.0.0.0", server_port=7860)

requirements.txt

@@ -1,9 +1,10 @@
 lean-interact
-ollama
+groq
 langchain
 langchain-community
-langchain-ollama
+langchain-groq
 langgraph
 faiss-cpu
 rank-bm25
 sentence-transformers
+gradio

src/langgraph_agent.py

@@ -176,7 +176,7 @@ def build_graph(lean_env: LeanEnvironment, retriever: MathLibRetriever, chain: R
 class LangGraphAgent:
     def __init__(
         self,
-        model_name: str = "qwen3-vl:4b",
+        model_name: str = "llama-3.3-70b-versatile",
         max_retries: int = 5,
         index_dir: str | None = None,
     ):

src/lmm_client.py

@@ -1,42 +1,36 @@
-import ollama
-from typing import List, Dict, Any, Optional
+from groq import Groq
+from typing import List, Optional
+
 
 class LMMClient:
     """
-    Client for interacting with local LMMs via Ollama.
-    Focuses on Qwen3-VL:4B for high-reasoning tasks.
+    Client for interacting with LLMs via Groq API.
     """
-    
-    def __init__(self, model_name: str = "qwen3-vl:4b"):
+
+    def __init__(self, model_name: str = "llama-3.3-70b-versatile"):
         self.model_name = model_name
+        self._client = Groq()
 
     def chat(self, prompt: str, system_prompt: Optional[str] = None) -> str:
-        """
-        Sends a chat request to the model.
-        """
         messages = []
         if system_prompt:
-            messages.append({'role': 'system', 'content': system_prompt})
-        
-        messages.append({'role': 'user', 'content': prompt})
-        
-        response = ollama.chat(
+            messages.append({"role": "system", "content": system_prompt})
+        messages.append({"role": "user", "content": prompt})
+
+        response = self._client.chat.completions.create(
             model=self.model_name,
-            messages=messages
+            messages=messages,
+            max_tokens=1024,
         )
-        return response['message']['content']
+        return response.choices[0].message.content
 
     def generate_proof_steps(self, lean_code: str, goals: List[str], errors: List[str]) -> str:
-        """
-        Specific helper to generate proof steps based on current Lean state.
-        """
         system_prompt = (
             "You are an expert Lean 4 proof assistant. "
             "Your goal is to complete the proof by replacing 'sorry' with valid Lean 4 code. "
             "Use Mathlib theorems where appropriate. "
             "Respond ONLY with the corrected Lean code block."
         )
-        
         prompt = f"""
 Current Lean Code:
 ```lean

src/rag_chain.py

@@ -3,7 +3,7 @@ from typing import List
 from langchain_core.documents import Document
 from langchain_core.output_parsers import StrOutputParser
 from langchain_core.prompts import ChatPromptTemplate
-from langchain_ollama import OllamaLLM
+from langchain_groq import ChatGroq
 
 
 _SYSTEM = """\
@@ -108,18 +108,12 @@ class RAGProofChain:
     LangChain LCEL chain: retrieved context + proof state → corrected Lean code.
     """
 
-    def __init__(self, model_name: str = "qwen3-vl:4b"):
+    def __init__(self, model_name: str = "llama-3.3-70b-versatile"):
         prompt = ChatPromptTemplate.from_messages([
             ("system", _SYSTEM),
             ("human", _HUMAN),
         ])
-        # Disable thinking/chain-of-thought mode (qwen3, gemma3) and cap output
-        # so the agent doesn't spend minutes generating reasoning tokens.
-        llm = OllamaLLM(
-            model=model_name,
-            num_predict=1024,           # cap response length
-            options={"think": False},   # disable thinking mode (qwen3/gemma3)
-        )
+        llm = ChatGroq(model=model_name, max_tokens=1024)
         self._chain = prompt | llm | StrOutputParser()
 
     def generate(