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.

The one thing to understand before using it: this screen may only reject. passed_screening means "no defect found by this harness". It is not a certification of faithfulness. Measured against 886 frozen human verdicts, statements a human reviewer had rejected still passed the full screen 17.0% of the time for theorems and 35.6% for definitions; statements a human had certified faithful were flagged 15–18% of the time. Every response carries this calibration verbatim.

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-…"
      }
    }
  }
}

What this does not guarantee

The judge configuration was calibrated 2026-07-15 against 886 frozen human verdicts (595 faithful / 291 unfaithful) from a production research-math corpus. Under strict two-judge consensus, human-rejected pairs still passed 17.0% (theorems) / 35.6% (definitions) of the time, and human-certified pairs were flagged 15–18% of the time. Both judges are Anthropic-family models, so correlated blind spots cannot be ruled out. The counterexample probe confabulates: on one PutnamBench sample its counterexamples were wrong 4 times out of 5. That calibration ran judge A on claude-opus-4-8; the shipped default is now claude-opus-5, and the recalibration against the frozen verdicts has not been run yet. Treat every flag as a candidate for human confirmation and every pass as "nothing found", never "faithful."

Human certification, meaning an expert reviewer confirming that the Lean means the informal statement, is what this screen deliberately does not automate. We offer it as a service: contact ibrahimnmian@gmail.com.

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.

Project page: millenniumresearch.ai/leanscreen