leanscreen

A calibrated faithfulness screen for informal↔Lean 4 statement pairs, on the
command line and over MCP, so you or
Claude (Code, Desktop, or any MCP client) can check statements while they
are being drafted.

$ leanscreen check Demo.lean
exists_perfect_number: REJECTED  lean=valid_in_our_env  flags=deterministic-vacuous:reflexive-goal [deterministic]
even_add_even: no defect found  lean=valid_in_our_env
screened 2 pair(s): 1 rejected, 0 needs human review, 1 passed screening (no defect found, not a certification)

That first theorem compiles and is even provable. Its docstring says "there
exists a natural number equal to the sum of its proper divisors"; its
statement says ∃ n : ℕ, n = n. The compiler has no objection. That gap is
what this tool screens for.

One rule governs everything below: this screen may only reject.
passed_screening means "no defect found by this harness", never
"faithful".

Two tools

check_fast is deterministic only: lints (unused binders, trivially
satisfiable existentials, pinned ∃! witnesses, suspicious ℕ-arithmetic,
and so on), vacuity checks (reflexive goals, True goals, withheld
declarations), and Lean 4 elaboration against your own mathlib environment.
Zero API calls, no key needed, about 0.1s per statement once the REPL is
warm. Call it constantly while drafting.

check_deep runs everything in check_fast, plus two independent LLM
judges under strict consensus (a back-translation judge and a
clause-by-clause checklist judge on separate models) and an adversarial
counterexample probe. It uses your own ANTHROPIC_API_KEY. Measured cost is
roughly $0.17–0.27 per statement, taking 30–60 seconds, and the response
reports actual spend as actual_cost_usd. Call it deliberately, before
something ships.

Both take informal (the natural-language statement), lean (the Lean 4
statement), and an optional kind (theorem | definition, inferred from
the declaration head when omitted). Responses rank their evidence:
counterexample > deterministic > two-judge-consensus > single-judge.
A single-judge flag is explicitly labeled as below the reporting bar.

Install

pip install leanscreen

Requires Python ≥3.12. Runtime dependencies are httpx, pydantic,
pydantic-settings, and mcp. Nothing else.

Command line

leanscreen check screens once and exits; the bare leanscreen command
still runs the MCP server. Three input shapes:

leanscreen check --informal "The sum of two even integers is even." --lean "theorem t (a b : Int) (ha : Even a) (hb : Even b) : Even (a + b)"

leanscreen check pairs.jsonl

leanscreen check MyFile.lean

The .lean form pairs each theorem/lemma/def with the /-- ... -/
doc comment above it and screens every documented declaration in the file;
undocumented declarations are skipped with a note. The default is the free
fast screen. --deep adds the judges and probe on your own
ANTHROPIC_API_KEY, with --budget USD as a hard stop. --json writes
one full payload object per line to stdout, everything else to stderr.

Exit codes are a CI contract: 0 means nothing was rejected (no defect
found, which is not a certification), 1 means at least one pair was
rejected on reject-tier evidence, 2 means a usage or configuration
error. A formalization repo can run leanscreen check src/*.lean in CI
and fail the build on unscreened defects.

Claude Code plugin

This repo is also a Claude Code plugin, and its own marketplace. Beyond
registering the MCP server for you, the plugin ships a skill that makes
Claude screen habitually: check_fast after drafting any Lean statement,
check_deep offered (with its cost stated) before formalizations ship, and
results always reported as screening rather than certification.

pip install leanscreen

then inside Claude Code:

/plugin marketplace add ibrahimmian36/leanscreen
/plugin install leanscreen@millennium-research

/leanscreen:screen <file> runs a fast pass over every pair in a file
(--deep opts into the paid judges after a cost confirmation). Uninstall
with /plugin uninstall leanscreen. The pip install still matters, since
the plugin launches the leanscreen command from your PATH.

Lean setup (optional but recommended)

Without a Lean project the server still runs; check_fast does lints +
vacuity and says plainly that elaboration was skipped. With one, statements
are elaborated for real:

1. A Lean 4 project with mathlib, built: lake build inside it.
2. The community REPL,
   built against the same toolchain: lake build inside the repl repo
   gives you .lake/build/bin/repl.
3. lake on the server's PATH.

mathlib imports once at server startup, taking about 100 seconds in the
background. Calls arriving mid-warm-up answer immediately with a "still
warming" note, then each check takes ~0.1s.

Configuration

Environment variables (or a .env in the working directory), all
LEANSCREEN_-prefixed:

Claude Code (.mcp.json in your project) or Claude Desktop
(claude_desktop_config.json):

{
  "mcpServers": {
    "lean-faithfulness-screen": {
      "command": "leanscreen",
      "env": {
        "LEANSCREEN_LEAN_PROJECT_PATH": "/path/to/your/lean-mathlib-project",
        "LEANSCREEN_LEAN_REPL_PATH": "/path/to/repl/.lake/build/bin/repl",
        "ANTHROPIC_API_KEY": "sk-ant-…"
      }
    }
  }
}

License

FSL-1.1-Apache-2.0 (the Functional Source License): free to use,
copy, modify, and redistribute, including internal commercial use,
non-commercial education and research, and professional services, but not
to offer as a competing commercial product or service. Each version
automatically becomes Apache 2.0 two years after its release, the same
license as mathlib. It is not OSI-approved until the conversion, so read it
before building on it commercially.

Provenance

Extracted from Millennium Research's private formalization platform
(2026-07-28); the detector stack, judge prompts, and calibration figures are
the ones behind our benchmark audits. The miniF2F and ProofNet# filings are
public, and the PutnamBench, ProofNetVerif, and CLEVER audits have been
shared with their maintainers. The calibration data is not included.

Human certification — an expert reviewer confirming the Lean means the
informal statement — is available as a service: contact
[email protected].

Project page: millenniumresearch.ai/leanscreen