# leanscreen

[![ci](https://github.com/ibrahimmian36/leanscreen/actions/workflows/ci.yml/badge.svg)](https://github.com/ibrahimmian36/leanscreen/actions/workflows/ci.yml)

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

```console
$ 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

```bash
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:

```bash
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)"
```

```bash
leanscreen check pairs.jsonl
```

```bash
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.

```bash
pip install leanscreen
```

then inside Claude Code:

```text
/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](https://github.com/leanprover-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:

| Variable | Default | Meaning |
|---|---|---|
| `LEANSCREEN_LEAN_PROJECT_PATH` | unset | Lean 4 + mathlib project (elaboration off when unset) |
| `LEANSCREEN_LEAN_REPL_PATH` | unset | community REPL binary; without it every check pays a full `lake env lean` |
| `LEANSCREEN_LEAN_TIMEOUT_SECONDS` | `180` | per-statement Lean budget |
| `LEANSCREEN_ANTHROPIC_MODEL` | `claude-opus-5` | judge A + probe (default postdates the 2026-07-15 calibration run) |
| `LEANSCREEN_JUDGE_B_MODEL` | `claude-fable-5` | checklist judge (calibrated default; locked-surface models get a 32k token budget automatically) |
| `LEANSCREEN_MAX_TOKENS` | `4096` | judge A response budget |
| `ANTHROPIC_API_KEY` | unset | needed for `check_deep` only |

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

```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](LICENSE) (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](https://millenniumresearch.ai/leanscreen)