Metadata-Version: 2.4
Name: leanscreen
Version: 0.1.0
Summary: A calibrated faithfulness screen for informal↔Lean 4 statement pairs, served over MCP. Screens only — never certifies.
Project-URL: Homepage, https://millenniumresearch.ai/leanscreen
Project-URL: Repository, https://github.com/ibrahimmian36/leanscreen
Author-email: Millennium Research <ibrahimnmian@gmail.com>
License: # Functional Source License, Version 1.1, Apache 2.0 Future License
        
        ## Abbreviation
        
        FSL-1.1-Apache-2.0
        
        ## Notice
        
        Copyright 2026 Millennium Research
        
        ## Terms and Conditions
        
        ### Licensor ("We")
        
        The party offering the Software under these Terms and Conditions.
        
        ### The Software
        
        The "Software" is each version of the software that we make available under
        these Terms and Conditions, as indicated by our inclusion of these Terms and
        Conditions with the Software.
        
        ### License Grant
        
        Subject to your compliance with this License Grant and the Patents,
        Redistribution and Trademark clauses below, we hereby grant you the right to
        use, copy, modify, create derivative works, publicly perform, publicly display
        and redistribute the Software for any Permitted Purpose identified below.
        
        ### Permitted Purpose
        
        A Permitted Purpose is any purpose other than a Competing Use. A Competing Use
        means making the Software available to others in a commercial product or
        service that:
        
        1. substitutes for the Software;
        
        2. substitutes for any other product or service we offer using the Software
           that exists as of the date we make the Software available; or
        
        3. offers the same or substantially similar functionality as the Software.
        
        Permitted Purposes specifically include using the Software:
        
        1. for your internal use and access;
        
        2. for non-commercial education;
        
        3. for non-commercial research; and
        
        4. in connection with professional services that you provide to a licensee
           using the Software in accordance with these Terms and Conditions.
        
        ### Patents
        
        To the extent your use for a Permitted Purpose would necessarily infringe our
        patents, the license grant above includes a license under our patents. If you
        make a claim against any party that the Software infringes or contributes to
        the infringement of any patent, then your patent license to the Software ends
        immediately.
        
        ### Redistribution
        
        The Terms and Conditions apply to all copies, modifications and derivatives of
        the Software.
        
        If you redistribute any copies, modifications or derivatives of the Software,
        you must include a copy of or a link to these Terms and Conditions and not
        remove any copyright notices provided in or with the Software.
        
        ### Disclaimer
        
        THE SOFTWARE IS PROVIDED "AS IS" AND WITHOUT WARRANTIES OF ANY KIND, EXPRESS OR
        IMPLIED, INCLUDING WITHOUT LIMITATION WARRANTIES OF FITNESS FOR A PARTICULAR
        PURPOSE, MERCHANTABILITY, TITLE OR NON-INFRINGEMENT.
        
        IN NO EVENT WILL WE HAVE ANY LIABILITY TO YOU ARISING OUT OF OR RELATED TO THE
        SOFTWARE, INCLUDING INDIRECT, SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES,
        EVEN IF WE HAVE BEEN INFORMED OF THEIR POSSIBILITY IN ADVANCE.
        
        ### Trademarks
        
        Except for displaying the License Details and identifying us as the origin of
        the Software, you have no right under these Terms and Conditions to use our
        trademarks, trade names, service marks or product names.
        
        ## Grant of Future License
        
        We hereby irrevocably grant you an additional license to use the Software under
        the Apache License, Version 2.0 that is effective on the second anniversary of
        the date we make the Software available. On or after that date, you may use the
        Software under the Apache License, Version 2.0, in which case the following
        will apply:
        
        Licensed under the Apache License, Version 2.0 (the "License"); you may not use
        this file except in compliance with the License.
        
        You may obtain a copy of the License at
        
        http://www.apache.org/licenses/LICENSE-2.0
        
        Unless required by applicable law or agreed to in writing, software distributed
        under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR
        CONDITIONS OF ANY KIND, either express or implied. See the License for the
        specific language governing permissions and limitations under the License.
License-File: LICENSE
Keywords: autoformalization,faithfulness,lean4,mathlib,mcp
Requires-Python: <3.14,>=3.12
Requires-Dist: httpx>=0.27.0
Requires-Dist: mcp<2,>=1.28.0
Requires-Dist: pydantic-settings>=2.3.0
Requires-Dist: pydantic>=2.7.0
Provides-Extra: dev
Requires-Dist: mypy>=1.10.0; extra == 'dev'
Requires-Dist: pytest>=8.2.0; extra == 'dev'
Requires-Dist: ruff>=0.5.0; extra == 'dev'
Description-Content-Type: text/markdown

# leanscreen

A calibrated faithfulness screen for informal↔Lean 4 statement pairs, served
over [MCP](https://modelcontextprotocol.io) so Claude (Code, Desktop, or any
MCP client) can check statements **while you draft them**.

**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`** — deterministic only: lints (unused binders, trivially
satisfiable existentials, pinned `∃!` witnesses, suspicious ℕ-arithmetic,
…), vacuity checks (reflexive goals, `True` goals, withheld declarations),
and Lean 4 elaboration against your own mathlib environment. **Zero API
calls, no key needed, ~0.1s per statement once the REPL is warm.** Call it
constantly while drafting.

**`check_deep`** — 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. Runs on **your** `ANTHROPIC_API_KEY`; measured cost is
roughly $0.17–0.27 per statement (the response reports actual spend as
`actual_cost_usd`), 30–60 seconds. 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`
— and a single-judge flag is explicitly labeled as below the reporting bar.

## Install

```bash
pip install git+https://github.com/ibrahimmian36/leanscreen
```

Requires Python ≥3.12. Runtime dependencies: `httpx`, `pydantic`,
`pydantic-settings`, `mcp` — nothing else.

## 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 (~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-4-8` | judge A + probe (the calibrated default) |
| `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-…"
      }
    }
  }
}
```

## 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. **Treat every flag as a candidate for human confirmation
and every pass as "nothing found", never "faithful."**

Human certification — 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](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). Not OSI-approved until the conversion — 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](https://millenniumresearch.ai/leanscreen)
