What can you do with this server?

leanscreen is an MCP server that screens informal↔Lean 4 statement pairs for faithfulness defects, helping you catch mismatches between natural-language claims and their formalizations. It provides two tools: * check_fast – Fast, deterministic checks (lints, vacuity/triviality, Lean elaboration) requiring no API key, ~0.1s per statement, ideal for constant use while drafting. Lint checks include unused binders, trivially satisfiable existentials, pinned ∃! witnesses, suspicious ℕ-arithmetic, and more; vacuity/triviality checks catch reflexive goals, True goals, withheld declarations; Lean 4 elaboration against your own mathlib environment when a REPL is configured. * check_deep – Full screen encompassing all check_fast checks plus two independent LLM judges (back-translation and clause-by-clause checklist on separate models) under strict consensus, and an adversarial counterexample probe. Requires an Anthropic API key; costs ~$0.17–0.27 per statement; takes 30–60 seconds. Reports actual API spend. Intended for deliberate use before formalizations ship. Both tools accept informal (natural language) and lean (Lean 4) inputs, with an optional kind (theorem or definition). Output includes a screening verdict: passed_screening (no defect found, not a certification) or REJECTED with flags. Evidence is ranked: counterexample > deterministic > two-judge-consensus > single-judge. The server can only reject, not certify faithfulness. Human-rejected pairs pass ~17% (theorems) / 35.6% (definitions) of the time; human-certified pairs are flagged 15–18%. Every flag is a candidate for human confirmation. Configure via environment variables (Lean project path, REPL path, Anthropic model, timeout, etc.). Use as a command-line tool, MCP server (for Claude Code/Desktop), or Claude Code plugin. Supports .lean files, command-line pairs, or JSONL input, and integrates with Lean+mathlib projects for real elaboration.

How do I use leanscreen?

1. Click on "Install Server". 2. Wait a few minutes for the server to deploy. Once ready, it will show a "Started" state. 3. In the chat, type @ followed by the MCP server name and your instructions, e.g., "@leanscreen Check if this Lean statement faithfully represents the informal text." That's it! The server will respond to your query, and you can continue using it as needed. Here is a step-by-step guide with screenshots.

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:

A Lean 4 project with mathlib, built: lake build inside it.
The community REPL, built against the same toolchain: lake build inside the repl repo gives you .lake/build/bin/repl.
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):

{
  "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

Available Tools

2 tools

check_deepA

Full faithfulness screen: everything in check_fast plus two independent LLM judges under strict consensus and an adversarial counterexample probe. Costs roughly 17–27¢ per statement (actual spend is reported in the response as actual_cost_usd) and takes 30–60 seconds — call it deliberately, before something ships. Requires ANTHROPIC_API_KEY.

This screen may only REJECT: an outcome of 'passed_screening' means no defect was found by this harness, NOT a certification of faithfulness (measured against human verdicts, human-rejected pairs still passed 17.0% of the time for theorems, 35.6% for definitions). Every flag — including a probe counterexample — is a candidate requiring human confirmation, not a verdict. The response ranks its evidence: a counterexample outranks a deterministic lint, which outranks two-judge consensus; a single-judge flag is below our own reporting bar.

kind is 'theorem' or 'definition'; omit it to infer from the Lean declaration head.

ParametersJSON Schema

Name	Required	Description	Default
`kind`	No
`lean`	Yes
`informal`	Yes

Output Schema

ParametersJSON Schema

Name	Required	Description
No output parameters

TDQS

A4.8/5.0

Behavior5/5

Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?

The description discloses all relevant behavioral traits: cost range, time, required API key, the meaning of a 'passed' outcome (not a certification), false pass rates for theorems and definitions, and the evidence ranking. Since no annotations are provided, the description carries the full burden and fulfills it thoroughly.

Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.

Conciseness5/5

Is the description appropriately sized, front-loaded, and free of redundancy?

The description is appropriately sized for the complexity of the tool. It is front-loaded with the core purpose and then provides additional details. Every sentence adds value without redundancy, and it maintains a clear structure.

Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.

Completeness4/5

Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?

Given the tool's complexity and that an output schema exists (but is not described here), the description covers most necessary aspects: behavior, cost, time, constraints, and interpretation of results. It could include more details on error conditions, but overall it is thorough for an AI agent to understand usage.

Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.

Parameters4/5

Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?

The description adds meaning for the 'kind' parameter by specifying it can be 'theorem' or 'definition' and if omitted it is inferred. For 'lean' and 'informal', the description does not elaborate beyond the tool's purpose, but given the context of faithfulness checking, their roles are deducible. Schema description coverage is 0%, so the description compensates partially.

Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.

Purpose5/5

Does the description clearly state what the tool does and how it differs from similar tools?

The description clearly states the tool's purpose: a full faithfulness screen that includes everything in check_fast plus two independent LLM judges and an adversarial counterexample probe. It distinguishes itself from the sibling tool check_fast by specifying the additional components.

Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.

Usage Guidelines5/5

Does the description explain when to use this tool, when not to, or what alternatives exist?

The description explicitly advises when to use this tool: 'call it deliberately, before something ships.' It contrasts with check_fast by noting the added thoroughness and cost, and warns about the time and expense (17-27¢, 30-60 seconds). This provides clear guidance on when to choose this tool over the sibling.

Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.

check_fastA

Deterministic faithfulness screen for one informal↔Lean 4 pair: lints, vacuity/triviality checks, and (when a Lean+mathlib REPL is configured and warm) elaboration. Free — no API calls, no key — and ~0.1s once the REPL is warm, so call it constantly while drafting. Catches statements that do not compile, trivially satisfiable existentials, vacuously-true specs, and claims hidden behind an unused declaration.

This screen may only REJECT: an outcome of 'passed_screening' means no defect was found by this harness — it is NOT a certification of faithfulness (measured against human verdicts, human-rejected pairs still passed the full screen 17.0% of the time for theorems, 35.6% for definitions). Every flag is a candidate for human confirmation, not a verdict.

kind is 'theorem' or 'definition'; omit it to infer from the Lean declaration head.

ParametersJSON Schema

Name	Required	Description	Default
`kind`	No
`lean`	Yes
`informal`	Yes

Output Schema

ParametersJSON Schema

Name	Required	Description
No output parameters

TDQS

A4.6/5.0

Behavior5/5

Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?

Since no annotations are provided, the description fully details behavioral traits: deterministic, no API calls, ~0.1s speed, REPL dependency, and crucially, its limitations with false pass rates (17% and 35.6%). This level of disclosure is exceptional and helps the agent set correct expectations.

Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.

Conciseness5/5

Is the description appropriately sized, front-loaded, and free of redundancy?

The description is well-structured with three focused paragraphs: functionality/speed, limitations/false pass rates, and parameter details. Every sentence adds value, no redundancy, and key information is front-loaded. It wastes no space while being comprehensive.

Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.

Completeness4/5

Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?

Given the existence of an output schema, the description appropriately omits return value details. It covers the tool's purpose, limitations, parameter semantics, and operational context. However, it lacks specificity on the exact input format for 'lean' (e.g., full file vs. snippet) and 'informal', which could be clarified for seamless use.

Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.

Parameters4/5

Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?

With 0% schema description coverage, the description adds significant meaning: it explains that 'kind' is 'theorem' or 'definition' and can be omitted for inference, and it contextualizes 'informal' and 'lean' as a pair. It does not fully detail the expected format or constraints for the two required strings, but provides enough for basic use.

Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.

Purpose5/5

Does the description clearly state what the tool does and how it differs from similar tools?

The description clearly defines the tool as a deterministic faithfulness screen for informal-to-Lean 4 pairs, listing specific checks (lints, vacuity, triviality) and emphasizing its speed and cost-free nature. It distinguishes itself from the sibling 'check_deep' by implying a fast, shallow check suitable for frequent use during drafting.

Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.

Usage Guidelines4/5

Does the description explain when to use this tool, when not to, or what alternatives exist?

The description provides strong usage context: 'call it constantly while drafting' and notes it is fast and free. However, it does not explicitly mention when to use the sibling 'check_deep' instead, leaving the comparison implicit rather than giving clear when-not guidance.

Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.

Tool Schema Changelog

Recent tool additions, removals, and schema changes observed during successful MCP inspections.

2 tool updatesv0.1.0Jul 28, 2026
- First observedcheck_deep
- First observedcheck_fast

Install Server

RayrunBuild, deploy, and operate MCP servers without becoming an infrastructure team.ray.runAd

TDQS

A4.6/5.0

Scored 2026-07-28 15:40 across 2 tools

Disambiguation5/5

The two tools are clearly distinct: check_fast is deterministic and free, suitable for frequent checks; check_deep includes LLM judges and costs money, appropriate for final verification. No overlap in purpose.

Naming Consistency5/5

Both tools use a consistent check_ prefix followed by a descriptive adjective (fast, deep), making their purposes clear and following a predictable pattern.

Tool Count4/5

With only 2 tools, the server is minimal but well-scoped for its purpose: one fast/deterministic screen and one deep/expensive screen. Could benefit from a medium option, but current count is reasonable.

Completeness4/5

The tools cover the essential workflow: fast frequent checks and deep pre-release verification. A minor gap is the lack of a certification tool, but the descriptions explicitly state neither tool certifies faithfulness, making this intentional.

Maintenance

ActivityMaintained

ResponsivenessNo issues

Resources

GitHub Repository

Need Help?

Related Servers

Unclaimed servers have limited discoverability.

Looking for Admin?

If you are the server author, to access and configure the admin panel.

Related MCP Connectors

rubrkit B
com.rubrkit
MCP-native AI evaluation: rubric audits, eval suites, and proof reports for AI/LLM output.
AI & Machine Learning Testing & QA Tools
412
injection-detector A
io.github.viridis-security
Formally-verified injection/exfiltration detector for AI agents (MCP-02).
Security Penetration Testing
22
Atomadic Forge
io.github.atomadictech
Architecture compiler for AI code. 11 tools, 92 actions, 872 Lean4 proofs, 100/100 self-cert.
Developer Tools Code Analysis AI & Machine Learning
21
DevSpeak
io.github.juanjaragavi
Official DevSpeak MCP server — translate technical text into formal specs from any AI IDE or agent
Developer Tools AI & Machine Learning Documentation Access
2

Related MCP Servers

math-logic-mcp
Code Execution Education & Learning Tools
ismailkerimov
A
license
A
quality
D
maintenance
MCP server that gives small LLMs verified symbolic-math & logic tools.
Updated 7 months ago (2026-02-20 12:40 UTC)
6
1
Apache 2.0
Chiasmus
Code Analysis Developer Tools
yogthos
A
license
Not graded
quality
A
maintenance
MCP server that gives LLMs access to formal verification via Z3 and SWI-Prolog, plus tree-sitter-based source code analysis. Translates natural language problems into formal logic using a template-based pipeline, verifies results with mathematical certainty, and analyzes call graphs for reachability, dead code, and impact analysis.
Updated 6 days ago (2026-09-04 19:34 UTC)
79
210
Apache 2.0
prova-mcp
AI & Machine Learning Autonomous Agents Code Execution
insinuateai
A
license
A
quality
D
maintenance
An MCP server that exposes the Prova reasoning verifier, enabling AI agents to verify their own reasoning and kernel-check Lean 4 proofs before outputting answers.
Updated 5 months ago (2026-04-19 16:30 UTC)
5
MIT
mathlas
Search Research & Data Developer Tools
Archerkattri
A
license
A
quality
A
maintenance
Airtight math tools an AI uses over MCP — 3.7M-theorem search, PSLQ constant ID, OEIS, real Lean kernel checks, applicability checklists. No LLM inside, no API key.
Updated 2 months ago (2026-07-25 01:10 UTC)
12
12
Apache 2.0

leanscreen

Two tools

Install

Command line

Claude Code plugin

Lean setup (optional but recommended)

Configuration

License

Provenance

Available Tools

Output Schema

TDQS

Output Schema

TDQS

Tool Schema Changelog

TDQS

Maintenance

Resources

Looking for Admin?

Related MCP Connectors

Related MCP Servers

math-logic-mcp

Chiasmus

prova-mcp

mathlas