(feat) local Lean4 engine with Docker-based execution

docs/source/ENGINES/formal_engine.md

@@ -1,8 +1,15 @@
-# Formal Engine (Axiom)
+# Formal Engine
 
-The Axiom engine provides Lean4 formal verification via the cloud-based Axle SDK. It supports proof checking, theorem extraction, proof repair, and more.
+The formal engine provides Lean4 formal verification with two backends:
 
-## Setup
+- **Axiom** (cloud) -- full-featured via the Axle SDK: proof checking, repair, theorem extraction, and more.
+- **Local** (Docker) -- runs the `lean` binary in a Docker container for type-checking and proof verification, with no cloud dependency.
+
+Both register as `engine="formal"`. Which one activates depends on the `FORMAL_ENGINE` config value.
+
+## Axiom (Cloud)
+
+### Setup
 
 1. Install the lean extras:
    ```bash
@@ -17,7 +24,7 @@ The Axiom engine provides Lean4 formal verification via the cloud-based Axle SDK
    }
    ```
 
-## Basic Usage
+### Basic Usage
 
 ```python
 from symai import Interface
@@ -41,9 +48,112 @@ result = axiom(lean_code, tool="extract_theorems")
 print(result.raw['documents'])
 ```
 
+### Tools Reference
+
+| Tool | Description |
+|---|---|
+| `check` | Check if Lean4 code is valid |
+| `verify_proof` | Verify a proof against a formal statement |
+| `extract_theorems` | Extract theorems from Lean4 code |
+| `rename` | Rename identifiers |
+| `theorem2lemma` | Convert theorems to lemmas |
+| `theorem2sorry` | Replace theorem proofs with sorry |
+| `merge` | Merge multiple Lean4 documents (takes `documents` arg) |
+| `simplify_theorems` | Simplify theorem statements |
+| `repair_proofs` | Attempt to repair broken proofs |
+| `have2lemma` | Convert have expressions to lemmas |
+| `have2sorry` | Replace have proofs with sorry |
+| `sorry2lemma` | Replace sorry placeholders with proofs |
+| `disprove` | Attempt to disprove a theorem |
+| `normalize` | Normalize Lean4 code |
+
+## Local (Docker)
+
+### Setup
+
+1. Install Docker and the lean extras:
+   ```bash
+   pip install symbolicai[lean]
+   ```
+
+2. Build the Lean4 Docker image (one-time):
+   ```bash
+   docker build -t lean4-container-image symai/backend/engines/formal/
+   ```
+
+3. Set your engine in `symai.config.json`:
+   ```json
+   {
+     "FORMAL_ENGINE": "local"
+   }
+   ```
+
+### Starting the server
+
+There are two ways to run the local Lean4 server:
+
+**Option A: Via symserver (recommended)**
+
+```bash
+symserver --lean4
+```
+
+This builds the Docker image if missing, finds a free port, and starts the FastAPI server. The server URL is saved to `symserver.config.json` so the engine discovers it automatically. Stop with Ctrl+C -- the Docker container is cleaned up automatically via `atexit`.
+
+**Option B: Auto-start**
+
+If no server is running, the engine auto-starts one on a free port when first used. No manual setup needed beyond the config and Docker image.
+
+### Basic Usage
+
+```python
+from symai import Interface
+
+lean = Interface('lean4_local')
+
+# Type-check Lean4 code
+result = lean("""
+theorem hello (a b : Prop) (ha : a) (hb : b) : a ∧ b := by
+  exact ⟨ha, hb⟩
+""")
+print(result.raw['status'])  # "success"
+print(result.raw['output'])  # "" (empty = no errors)
+
+# Invalid code returns "failure" with error details
+result = lean("""
+theorem bad (n : Nat) : n + 1 = n := by
+  omega
+""")
+print(result.raw['status'])  # "failure"
+print(result.raw['output'])  # "omega could not prove the goal..."
+```
+
+The local engine passes your code directly to `lean` inside the Docker container. Everything the `lean` binary supports works: `#check`, `#eval`, `#print`, theorems, definitions, structures, typeclasses, etc.
+
+### Architecture
+
+```
+Interface("lean4_local")
+    └─ Lean4LocalEngine (HTTP client)
+          └─ POST /check  ─────►  lean4_fastapi (FastAPI server)
+                                       └─ ContainerManager
+                                             └─ docker exec lean <file>
+```
+
+- **Lean4LocalEngine** -- HTTP client that discovers or auto-starts the server.
+- **lean4_fastapi** -- FastAPI server managing a Docker container with a 5-minute idle timeout.
+- **ContainerManager** -- creates/reuses a `lean4-server-container`, executes code via `docker exec`.
+
+### Server discovery order
+
+The engine resolves the server URL in this order:
+
+1. `url` in `symserver.config.json` (set automatically by `symserver --lean4`)
+2. Auto-start a new server on a free port
+
 ## Using with `@contract`
 
-Each contract's post-condition can delegate LLM outputs to Axiom's Lean4 engine for formal verification before accepting them. The `@contract` decorator calls the LLM (using the `prompt` property and the data models), then runs `post()` to validate. If `post()` raises, the contract feeds the error back to the LLM and retries.
+Each contract's post-condition can delegate LLM outputs to the formal engine for verification before accepting them. The `@contract` decorator calls the LLM (using the `prompt` property and the data models), then runs `post()` to validate. If `post()` raises, the contract feeds the error back to the LLM and retries.
 
 ```python
 from pydantic import Field
@@ -121,22 +231,3 @@ class ProveTheorem(Expression):
 ```
 
 See [`examples/formal_verification.ipynb`](../../../examples/formal_verification.ipynb) for a full runnable example.
-
-## Tools Reference
-
-| Tool | Description |
-|---|---|
-| `check` | Check if Lean4 code is valid |
-| `verify_proof` | Verify a proof against a formal statement |
-| `extract_theorems` | Extract theorems from Lean4 code |
-| `rename` | Rename identifiers |
-| `theorem2lemma` | Convert theorems to lemmas |
-| `theorem2sorry` | Replace theorem proofs with sorry |
-| `merge` | Merge multiple Lean4 documents (takes `documents` arg) |
-| `simplify_theorems` | Simplify theorem statements |
-| `repair_proofs` | Attempt to repair broken proofs |
-| `have2lemma` | Convert have expressions to lemmas |
-| `have2sorry` | Replace have proofs with sorry |
-| `sorry2lemma` | Replace sorry placeholders with proofs |
-| `disprove` | Attempt to disprove a theorem |
-| `normalize` | Normalize Lean4 code |

pyproject.toml

@@ -6,7 +6,14 @@ build-backend = "setuptools.build_meta"
 package = true
 required-version = ">=0.9.17"
 exclude-newer = "7 days"
-constraint-dependencies = ["pyjwt>=2.12.0", "pyasn1>=0.6.3"]
+constraint-dependencies = [
+    "pyjwt>=2.12.0",
+    "pyasn1>=0.6.3",
+    "aiohttp>=3.13.4",       # CVE: unlimited trailer headers, multipart bypass, SSRF, duplicate host headers, etc.
+    "anthropic>=0.87.0",     # CVE: memory tool race condition + insecure file permissions
+    "cryptography>=46.0.6",  # CVE: incomplete DNS name constraint enforcement
+    "pygments>=2.20.0",      # CVE: ReDoS via inefficient GUID regex
+]
 
 [project]
 name = "symbolicai"
@@ -30,14 +37,14 @@ dependencies = [
     "setuptools>=70.0.0",
     "toml>=0.10.2",
     "loguru>=0.7.3",
-    "aiohttp>=3.11.13",
+    "aiohttp>=3.13.4",
     "numpy>=1.26.4,<=2.1.3",
     "tqdm>=4.66.3",
     "python-box>=7.1.1",
     "torch<2.10.0", # weird errors, things like "no torch.Tensor"
     "sympy>=1.12",
     "openai>=1.60.0",
-    "anthropic>=0.43.1",
+    "anthropic>=0.87.0",
     "google-genai>=1.16.1",
     "ipython>=8.24.0",
     "tiktoken>=0.8.0",
@@ -63,7 +70,7 @@ hf           = ["transformers>=4.45.2", "accelerate>=0.33.0", "peft>=0.13.1", "d
 scrape       = ["beautifulsoup4>=4.12.3", "trafilatura>=2.0.0", "pdfminer.six", "playwright>=1.45.0", "parallel-web>=0.3.3"]
 llama_cpp    = ["llama-cpp-python[server]>=0.3.7"] # handle separately since this dependency may not compile and require special maintenance
 wolframalpha = ["wolframalpha>=5.0.0"]
-lean         = ["docker>=7.0.0", "paramiko>=3.4.0", "axiom-axle>=1.0.0"]
+lean         = ["docker>=7.0.0", "axiom-axle>=1.0.0"]
 whisper      = ["openai-whisper>=20240930", "numba>=0.62.1", "llvmlite>=0.45.1"]
 search       = ["firecrawl-py>=4.12.0", "parallel-web>=0.3.3", "tldextract>=5.1.0"]
 serpapi      = ["google_search_results>=2.4.2"]

symai/__init__.py

@@ -152,6 +152,7 @@ def _save_symserver_config(config: dict, *, include_home: bool = False) -> None:
         "qdrant" in arg.lower() or arg in _QDRANT_SERVER_FLAGS for arg in sys.argv[1:]
     )
     rag_requested = any(arg == "--rag" or arg.startswith("--rag-api") for arg in sys.argv[1:])
+    lean4_requested = "--lean4" in sys.argv[1:]
     uvicorn_reload_default = os.getenv("UVICORN_RELOAD", "").strip().lower() in {
         "1",
         "true",
@@ -348,7 +349,7 @@ def _wait_for_qdrant(
                         raise RuntimeError(msg)
                 time.sleep(0.25)
         except KeyboardInterrupt:
-            UserMessage("Server stopped!")
+            UserMessage("Server stopped.", style="success")
         except Exception as e:
             UserMessage(f"Error running server: {e}")
         finally:
@@ -390,7 +391,7 @@ def _wait_for_qdrant(
         try:
             subprocess.run(command, check=True)
         except KeyboardInterrupt:
-            UserMessage("Server stopped!")
+            UserMessage("Server stopped.", style="success")
         except Exception as e:
             UserMessage(f"Error running server: {e}")
         finally:
@@ -410,12 +411,41 @@ def _wait_for_qdrant(
         try:
             command(host=args.host, port=args.port)
         except KeyboardInterrupt:
-            UserMessage("Server stopped!")
+            UserMessage("Server stopped.", style="success")
         except Exception as e:
             UserMessage(f"Error running server: {e}")
         finally:
             _symserver_config_["online"] = False
             _save_symserver_config(_symserver_config_)
+
+    elif lean4_requested:
+        # Lean4 server - check FORMAL_ENGINE and start container + FastAPI
+        from .server.lean4_server import lean4_server  # noqa
+
+        command, args = lean4_server()
+        _symserver_config_.update(zip(args[::2], args[1::2], strict=False))
+        _symserver_config_["online"] = True
+
+        # Extract port from command (uvicorn --port X)
+        port = 8000
+        for i, arg in enumerate(command):
+            if arg == "--port" and i + 1 < len(command):
+                port = int(command[i + 1])
+                break
+        _symserver_config_["url"] = f"http://localhost:{port}"
+
+        _save_symserver_config(_symserver_config_, include_home=True)
+
+        try:
+            subprocess.run(command, check=True)
+        except KeyboardInterrupt:
+            UserMessage("Server stopped.", style="success")
+        except Exception as e:
+            UserMessage(f"Error running server: {e}")
+        finally:
+            _symserver_config_["online"] = False
+            _save_symserver_config(_symserver_config_)
+
     else:
         msg = (
             "You're trying to run a local server without a recognised engine configuration. "
@@ -424,7 +454,8 @@ def _wait_for_qdrant(
             "or pass any qdrant_server flag (e.g. symserver --docker-detach)\n"
             "  - llama.cpp (neuro-symbolic):    set NEUROSYMBOLIC_ENGINE_MODEL=llamacpp or "
             "EMBEDDING_ENGINE_MODEL=llamacpp in symai.config.json\n"
-            "  - HuggingFace (neuro-symbolic):  set NEUROSYMBOLIC_ENGINE_MODEL=huggingface in symai.config.json"
+            "  - HuggingFace (neuro-symbolic):  set NEUROSYMBOLIC_ENGINE_MODEL=huggingface in symai.config.json\n"
+            "  - Lean4 (formal):                symserver --lean4 (requires FORMAL_ENGINE=local)"
         )
         UserMessage(msg, raise_with=ValueError)
 

symai/backend/engines/formal/Dockerfile

@@ -0,0 +1,16 @@
+FROM buildpack-deps:bookworm
+
+ENV ELAN_HOME=/usr/local/elan \
+    PATH=/usr/local/elan/bin:$PATH \
+    LEAN_VERSION=leanprover/lean4:nightly
+
+RUN apt-get update && apt-get install -y curl && rm -rf /var/lib/apt/lists/*
+
+RUN curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain $LEAN_VERSION && \
+    elan default $LEAN_VERSION && \
+    elan --version && \
+    lean --version && \
+    leanc --version && \
+    lake --version
+
+CMD ["sleep", "infinity"]