check_deep
Performs a deep faithfulness screen on informal-Lean statement pairs using two independent LLM judges and an adversarial counterexample probe to detect defects before shipping.
Instructions
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.
Input Schema
| Name | Required | Description | Default |
|---|---|---|---|
| kind | No | ||
| lean | Yes | ||
| informal | Yes |
Output Schema
| Name | Required | Description | Default |
|---|---|---|---|
No arguments | |||