`api_lean_check`

Ask a configured host (native, Node Wasm, or the isolated browser Lean Wasm page) to compile exact Bosatsu sources and run pinned Lean on supported Yichus/Law obligations. Pass sources to check, or receipt_sha256 alone to fetch the exact full receipt cached by this host. The compact view is the default agent result; view full returns the complete validated run. Its fullReceiptSha256 names exact full receipt bytes, not a portable proof: recompile and recheck across builds. The translator requires a direct Law.check and exactly one direct filled Witness. All three hosts support capture-free nonrecursive unary Bool predicates and a narrow structural List[Bool] predicate with self-calls only on the bound tail of a Nil/Cons match. The native host also supports a checked Int/product grammar with exported literal lean_proof and lean_witness scripts and the optional pinned Mathlib bundle. Lean checks generated recursion termination; author proof terms can cite existing Mathlib theorems. Mathlib is unavailable in the Node/browser Wasm runtime. Verified means generated law and witness theorems passed Lean elaboration and axiom audit over the recorded input type. Native receipts also record independent leanchecker replay; Wasm receipts explicitly set independentKernelReplay false. Compare method, scope, and completion before describing the proof. FiniteObligation is not admitted. A compact not-admitted row means this method could not check the law: withhold proof-dependent changes and seek another proof route. A not-verified row means Lean did not establish proof; inspect the full receipt. Unsupported laws, missing tools, timeouts, and empty obligation sets are inconclusive. The isolated browser Lean page supports the Wasm route through WebMCP; the general browser workbench reports unsupported-host guidance. Worked sources: https://yich.us/reference/api-mcp/examples.html#lean-bool and https://yich.us/reference/api-mcp/examples.html#lean-list and https://yich.us/reference/api-mcp/examples.html#lean-mathlib.

Kind: LeanCheck. Origin: Yichus/Mcp::catalog.

CLI: yichus lean — host-only pinned Lean proof of supported Bool and structural List[Bool] laws; npm MCP requires an explicitly configured proof host; browser WebMCP reports unsupported host.

Parameters

sources (optional, array) — JSON array of {fileName, source} Bosatsu files including exported Obligation bindings; required unless fetching receipt_sha256.
receipt_sha256 (optional, string) — Fetch the exact full receipt from this live host by the compact view's fullReceiptSha256; omit sources.
view (optional, string) — compact (default) or full; receipt retrieval always returns full.
timeout_ms (optional, integer) — Optional whole-worker deadline in milliseconds (default 180000).

Read the result according to this tool’s scope: static checks, bounded execution checks, and descriptive diagrams answer different questions. A successful call is not a general approval of the program. The safety and permissions guide compares the checks and provides editable ownership, guard, and role examples.