Snapkitty/lean-llm-starter

Lean LLM Starter

LLMs propose. Lean verifies.

A deterministic Lean 4 verification harness for LLM-generated proofs.

This repository treats the language model as an untrusted proposal engine and Lean 4 as the trusted verification kernel.

The model may suggest a proof.

Lean decides whether the proof is valid.

Operator Intent
      ↓
Prolog Authorization Gate
      ↓
LLM Proof Proposal
      ↓
Schema Validation
      ↓
Lean 4 Parse and Verification
      ↓
Verified Artifact or Deterministic Rejection

Purpose

Most LLM proof systems rely too heavily on the model's own output.

This repository uses a stricter trust boundary:

• The LLM proposes proof artifacts
• Prolog enforces execution and authorization rules
• Lean 4 parses and verifies the proof
• Invalid or incomplete proofs are rejected
• Verification results can be exported into WORM-ready audit records

The goal is not to trust generated mathematics.

The goal is to verify it.

Architecture

Lean 4

The Lean layer is the trusted mathematical kernel.

It is responsible for:

• Parsing generated proof artifacts
• Validating theorem structure
• Rejecting unsupported syntax
• Blocking sorry
• Rejecting malformed Lean 3 syntax
• Type-checking submitted proofs
• Producing deterministic verification results

Prolog

The Prolog layer acts as the governance and control surface.

It is responsible for:

• Authorization checks
• Schema validation
• Retry control
• Verification routing
• Execution policy
• Rejection of unauthorized runs

LLM Inference

The inference layer is intentionally untrusted.

It may use Granite, Llemma, llama.cpp-compatible servers, vLLM-compatible backends, or another local model.

Its only job is to propose proof steps in the expected schema.

It does not determine correctness.

Evaluation Harness

The evaluation layer runs generated proofs through the Lean kernel and records whether they pass or fail.

The included harness supports MiniF2F-style theorem evaluation and local reproducibility.

Repository Structure

lean-llm-starter/
├── eval/
│   ├── requirements.txt
│   └── run_minif2f.py
├── fixtures/
│   └── sample_input.jsonl
├── inference/
│   ├── Dockerfile
│   ├── requirements.txt
│   ├── prompt.txt
│   └── server.py
├── infra/
│   └── verification-loop/
│       ├── .env.example
│       └── docker-compose.yml
├── lean4/
│   ├── lakefile.toml
│   ├── lean-toolchain
│   ├── MiniF2F.lean
│   ├── VerifyMain.lean
│   └── src/
│       └── SovereignCorpus/
│           ├── Bridge/
│           │   ├── Granite4Parser.lean
│           │   └── Granite4Schema.lean
│           ├── Core.lean
│           └── Tactics/
│               └── PlasmaGate.lean
├── logic/
│   ├── sovereign_verification.pl
│   └── verification_loop.pl
├── hf/
│   └── README.md
├── docker-compose.yml
├── Makefile
└── LICENSE

Core Trust Model

The system separates proposal, policy, and proof.

LLM
Untrusted proposal generation

Prolog
Policy, authorization, and orchestration

Lean 4
Trusted proof verification

Audit Layer
Receipt generation and permanent evidence

No proof is accepted because an LLM says it is correct.

A proof is accepted only when Lean successfully checks it.

Included Components

• Lean 4 proof verification kernel
• Granite-style JSON proof schema
• Lean-side parser
• Lean 3 syntax guards
• sorry rejection
• Prolog authorization layer
• Prolog retry loop
• Local inference server wrapper
• Dockerized inference runtime
• MiniF2F-style evaluation harness
• Sample JSONL theorem fixture
• Hugging Face publishing structure
• WORM-ready verification output design

Quick Start

Build the Lean Project

cd lean4
lake update
lake build

On Windows, when lake is not available through the system path:

C:\Users\jessi\.elan\bin\lake.exe update
C:\Users\jessi\.elan\bin\lake.exe build

Run the Parser Smoke Test

cd lean4
lake exe verify -- --parse ../fixtures/sample_input.jsonl

Start the Inference Service

cd inference
docker build -t lean-llm-inference .
docker run -d \
  -p 8080:8080 \
  --name lean-llm-inference \
  lean-llm-inference

Run the Evaluation Harness

cd eval
pip install -r requirements.txt
python run_minif2f.py

Start the Verification Infrastructure

docker compose \
  --env-file infra/verification-loop/.env.example \
  up -d

Run the Prolog Verification Loop

swipl -g "verify_with_retries(
  'theorem demo : True := by trivial',
  'ED25519_SIG',
  3,
  Result
), writeln(Result), halt" logic/verification_loop.pl

Proof Artifact Schema

Generated proof proposals are exchanged using structured JSON rather than unrestricted model output.

Example shape:

{
  "id": "demo-problem-1",
  "statement": "theorem demo_nonneg (x : ℝ) : x ^ 2 ≥ 0",
  "context": [
    "import Mathlib"
  ],
  "tacticHint": "nlinarith",
  "meta": {
    "source": "granite-verifier",
    "operatorSig": "ED25519_SIG_PLACEHOLDER",
    "maxSteps": 30,
    "allowedTactics": [
      "rw",
      "simp_all",
      "norm_num",
      "linarith",
      "nlinarith",
      "aesop",
      "apply",
      "exact",
      "intro",
      "cases",
      "induction",
      "constructor",
      "field_simp",
      "ring_nf",
      "omega"
    ]
  }
}

The schema constrains what the model is allowed to submit and gives the verifier a deterministic interface.

Design Principles

Evidence Over Confidence

A fluent answer is not evidence.

A Lean-checked proof is.

Deterministic Rejection

Malformed, incomplete, unauthorized, or unverifiable proof artifacts must fail closed.

Local-First Verification

The verification kernel can run independently from hosted model providers.

Separation of Concerns

The model proposes.

The governance layer controls.

The theorem prover verifies.

The audit layer records.

No Trusted Model Assumption

The architecture does not depend on the LLM being honest, aligned, deterministic, or correct.

What This Repository Is

This repository is:

• A Lean-backed LLM proof gateway
• A local theorem verification harness
• A structured interface between language models and formal proof
• A foundation for sovereign mathematical agents
• A reproducible proof evaluation environment
• A verification-first AI architecture

What This Repository Is Not

This repository is not:

• A finished autonomous theorem prover
• A claim that all LLM output is reliable
• A replacement for Lean's kernel
• A guarantee that generated proofs will succeed
• A repository of pretrained model weights
• A system that accepts natural-language confidence as mathematical evidence

Current Scope

The current implementation provides the verification structure and execution path required to:

1. Receive a theorem or proof request
2. Route it through policy controls
3. Generate a structured proof proposal
4. Parse the proposal
5. Submit it to Lean
6. Accept or reject it deterministically
7. Preserve the result as an auditable artifact

Future Work

Planned extensions may include:

• Expanded MiniF2F coverage
• Multiple local inference backends
• Stronger proof-step schemas
• Ed25519-signed verification receipts
• Append-only WORM evidence logs
• Proof repair loops
• Tactic allowlists per theorem class
• Resource limits for generated proofs
• Air-gapped execution profiles
• Formal verification of the orchestration layer
• Interactive proof verification UI
• Hugging Face model and Space publication
• Benchmark dashboards
• Multi-model proof proposal comparison

Hugging Face Readiness

The repository includes:

• Git LFS configuration for model artifacts
• A model card template
• Publishing documentation
• Separation between model weights and verifier code
• Infrastructure suitable for an interactive verification Space

Recommended publication structure:

Repository 1
Lean verification harness

Repository 2
Model weights or adapters

Repository 3
Interactive proof verification Space

Security Model

Generated proof content must be treated as hostile input.

Recommended deployment controls include:

• Container isolation
• Strict tactic allowlists
• CPU and memory limits
• Execution timeouts
• No unrestricted shell access
• No arbitrary imports
• Signed operator requests
• Immutable verification receipts
• Pinned Lean toolchains
• Pinned container images
• Reproducible builds

Status

This repository is an active verification scaffold.

The Lean project, parser, inference wrapper, Prolog governance layer, evaluation harness, Docker topology, and structured proof interface establish the foundation for deterministic LLM-assisted theorem verification.

The architecture is intentionally conservative:

No proof.
No acceptance.

No evidence.
No claim.

License

This repository is distributed under the license included in the LICENSE file.

Model weights, external datasets, and third-party theorem corpora may be subject to separate licenses.

Author

Ahmad Ali Parr SNAPKITTYWEST SnapKitty Collective

Principle

The language model may propose the mathematics. The kernel must prove it.