Schema | leanscreen

leanscreen

Overview Schema Source Related Servers Score Discussions Admin

Server Configuration

Describes the environment variables required to run the server.

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

Instructions

Guidance the server publishes about itself, which clients place ahead of the tool catalog so the model reads it before choosing anything.

This server publishes no instructions, or was last inspected before Glama recorded them.

Capabilities

Features and capabilities supported by this server

Protocol revision2025-11-25

Capability	Details
`tools`	{ "listChanged": false }
`prompts`	{ "listChanged": false }
`resources`	{ "subscribe": false, "listChanged": false }
`experimental`	{}

Tools

Functions exposed to the LLM to take actions

Name Description

Name	Description
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.
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.

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.

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.

Prompts

Interactive templates invoked by user choice

Name	Description
No prompts

Resources

Contextual data attached and managed by the client

Name	Description
No resources

Server Configuration
Instructions
Capabilities
Tools
Prompts
Resources