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.

Related MCP server: Chiasmus

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 ibrahimnmian@gmail.com.

Project page: millenniumresearch.ai/leanscreen