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.
Tool call template
Replace each placeholder with a value matching the input schema. Only required parameters are included; add optional parameters as needed.
{
"id": 1,
"jsonrpc": "2.0",
"method": "tools/call",
"params": {
"arguments": {
"informal": "<informal>",
"lean": "<lean>"
},
"name": "check_deep"
}
}Input Schema
| Name | Required | Description | Default |
|---|---|---|---|
| kind | No | ||
| lean | Yes | ||
| informal | Yes |
Output Schema
| Name | Required | Description | Default |
|---|---|---|---|
No arguments | |||