Add Claude API support (users supply their own key)

Users can now pick a Claude model (Opus 4.7, Sonnet 4.6, Haiku 4.5) from
the model dropdown and paste their own Anthropic API key into a password
field above the editors. Groq remains the default (using the Space's
GROQ_API_KEY env var).

Implementation:
- `RAGProofChain` picks provider from model name prefix:
`claude-*` → ChatAnthropic, everything else → ChatGroq
- `api_key` parameter threaded through LangGraphAgent → RAGProofChain
so user-provided keys reach the LangChain client directly (never set
as an env var, so concurrent calls don't clobber each other)
- `solve_proof` validates: Claude models require the key field; Groq
models still rely on the Space's env var
- New deps: `langchain-anthropic`
- Test mocks accept **kwargs so the existing fuzz/concurrent suites still
pass with the new constructor signature

The Anthropic key is sent over HTTPS to the Space backend then to
Anthropic; it is not stored on disk and is not logged.

app.py

@@ -81,6 +81,18 @@ GROQ_MODELS = [
     "llama-3.1-8b-instant",
 ]
 
+CLAUDE_MODELS = [
+    "claude-opus-4-7",
+    "claude-sonnet-4-6",
+    "claude-haiku-4-5-20251001",
+]
+
+ALL_MODELS = GROQ_MODELS + CLAUDE_MODELS
+
+
+def _is_claude(model_name: str) -> bool:
+    return model_name.startswith("claude-")
+
 EXAMPLE_CODE = """\
 import Mathlib
 
@@ -336,12 +348,19 @@ input[type="range"] { accent-color: var(--accent) !important; }
 """
 
 
-def solve_proof(lean_code: str, model_name: str, max_retries: int):
+def solve_proof(lean_code: str, model_name: str, max_retries: int, anthropic_api_key: str = ""):
     if not lean_code.strip():
         return _status_html("idle", "No input — paste a Lean 4 theorem on the left."), "", ""
 
-    if not os.environ.get("GROQ_API_KEY"):
-        return _status_html("err", "GROQ_API_KEY missing — add it as a Space secret."), "", ""
+    claude = _is_claude(model_name)
+    if claude:
+        if not anthropic_api_key or not anthropic_api_key.strip():
+            return _status_html("err", "Anthropic API key required for Claude models — paste it above."), "", ""
+        api_key = anthropic_api_key.strip()
+    else:
+        if not os.environ.get("GROQ_API_KEY"):
+            return _status_html("err", "GROQ_API_KEY missing — add it as a Space secret."), "", ""
+        api_key = None  # ChatGroq picks it up from env
 
     tmp_path = None
     try:
@@ -354,7 +373,11 @@ def solve_proof(lean_code: str, model_name: str, max_retries: int):
 
         log_buf = io.StringIO()
         with _capture_stdout(log_buf):
-            agent = LangGraphAgent(model_name=model_name, max_retries=int(max_retries))
+            agent = LangGraphAgent(
+                model_name=model_name,
+                max_retries=int(max_retries),
+                api_key=api_key,
+            )
             result = agent.solve_file_detailed(tmp_path)
 
         with open(tmp_path, encoding="utf-8") as f:
@@ -415,13 +438,21 @@ with gr.Blocks(
     # ─── Controls bar ───────────────────────────────────────────────
     with gr.Row(elem_id="controls"):
         model_dropdown = gr.Dropdown(
-            choices=GROQ_MODELS, value=GROQ_MODELS[0],
+            choices=ALL_MODELS, value=GROQ_MODELS[0],
             label="Model", show_label=True, container=False, scale=2,
         )
         retries_slider = gr.Slider(
             minimum=1, maximum=10, value=5, step=1,
             label="Max retries", show_label=True, container=False, scale=1,
         )
+        anthropic_key_input = gr.Textbox(
+            label="Anthropic API key (only for Claude models)",
+            placeholder="sk-ant-…",
+            type="password",
+            show_label=True,
+            container=False,
+            scale=2,
+        )
 
     # ─── Two editor panes ───────────────────────────────────────────
     with gr.Row(elem_id="editor-row", equal_height=True):
@@ -462,12 +493,12 @@ with gr.Blocks(
     # ─── Wiring ─────────────────────────────────────────────────────
     solve_btn.click(
         solve_proof,
-        inputs=[lean_input, model_dropdown, retries_slider],
+        inputs=[lean_input, model_dropdown, retries_slider, anthropic_key_input],
         outputs=[status_output, code_output, logs_output],
     )
     regen_btn.click(
         solve_proof,
-        inputs=[lean_input, model_dropdown, retries_slider],
+        inputs=[lean_input, model_dropdown, retries_slider, anthropic_key_input],
         outputs=[status_output, code_output, logs_output],
     )
     reset_btn.click(lambda: EXAMPLE_CODE, outputs=lean_input)

requirements.txt

@@ -3,6 +3,7 @@ groq
 langchain
 langchain-community
 langchain-groq
+langchain-anthropic
 langchain-huggingface
 langchain-classic
 langgraph

src/langgraph_agent.py

@@ -212,10 +212,11 @@ class LangGraphAgent:
         model_name: str = "llama-3.3-70b-versatile",
         max_retries: int = 5,
         index_dir: str | None = None,
+        api_key: str | None = None,
     ):
         self._lean_env = LeanEnvironment(use_mathlib=True)
         self._retriever = MathLibRetriever(index_dir=index_dir)
-        self._chain = RAGProofChain(model_name=model_name)
+        self._chain = RAGProofChain(model_name=model_name, api_key=api_key)
         self._graph = build_graph(self._lean_env, self._retriever, self._chain)
         self._max_retries = max_retries
 

src/rag_chain.py

@@ -1,9 +1,10 @@
-from typing import List
+from typing import List, Optional
 
 from langchain_core.documents import Document
 from langchain_core.output_parsers import StrOutputParser
 from langchain_core.prompts import ChatPromptTemplate
 from langchain_groq import ChatGroq
+from langchain_anthropic import ChatAnthropic
 
 
 _SYSTEM = """\
@@ -95,6 +96,23 @@ Provide the corrected Lean code that solves all goals and fixes all errors.
 """
 
 
+def _make_llm(model_name: str, api_key: Optional[str]):
+    """
+    Pick the chat LLM provider from the model name:
+      - `claude-*` → Anthropic (requires user-provided api_key)
+      - everything else → Groq (api_key optional; falls back to GROQ_API_KEY env)
+    """
+    if model_name.startswith("claude-"):
+        kwargs = {"model": model_name, "max_tokens": 1024}
+        if api_key:
+            kwargs["anthropic_api_key"] = api_key
+        return ChatAnthropic(**kwargs)
+    kwargs = {"model": model_name, "max_tokens": 1024}
+    if api_key:
+        kwargs["groq_api_key"] = api_key
+    return ChatGroq(**kwargs)
+
+
 def _format_docs(docs: List[Document]) -> str:
     if not docs:
         return "(none retrieved)"
@@ -108,12 +126,12 @@ class RAGProofChain:
     LangChain LCEL chain: retrieved context + proof state → corrected Lean code.
     """
 
-    def __init__(self, model_name: str = "llama-3.3-70b-versatile"):
+    def __init__(self, model_name: str = "llama-3.3-70b-versatile", api_key: Optional[str] = None):
         prompt = ChatPromptTemplate.from_messages([
             ("system", _SYSTEM),
             ("human", _HUMAN),
         ])
-        llm = ChatGroq(model=model_name, max_tokens=1024)
+        llm = _make_llm(model_name, api_key)
         self._chain = prompt | llm | StrOutputParser()
 
     def generate(

tests/test_app_fuzz.py

@@ -48,7 +48,7 @@ class _DummyAgent:
     last_path: str | None = None
     last_bytes: bytes | None = None
 
-    def __init__(self, model_name="x", max_retries=5):
+    def __init__(self, model_name="x", max_retries=5, **kwargs):
         self.model_name = model_name
         self.max_retries = max_retries
         _DummyAgent.init_log.append((model_name, max_retries))

tests/test_concurrent_solve.py

@@ -39,7 +39,7 @@ class _DummyAgent:
     # Optional: tag to print so we can detect cross-thread stdout bleed.
     print_tag: bool = False
 
-    def __init__(self, model_name="x", max_retries=5):
+    def __init__(self, model_name="x", max_retries=5, **kwargs):
         self.model_name = model_name
         self.max_retries = max_retries