Verify formal (real Lean kernel)
verify_formalCheck Lean 4 proofs and snippets with the actual kernel. Submit a statement and proof for verification, or a full snippet for typechecking.
Instructions
Run the REAL Lean 4 kernel (NO LLM). Two modes: (1) pass lean (a full snippet, e.g. 'example : 2 + 2 = 4 := rfl') to typecheck it as-is; (2) pass proof to PROOF-CHECK — statement must then be the Lean 4 proposition and proof YOUR proof (term or 'by ...' tactic block); mathlas builds theorem _mathlas_check : <statement> := <proof> and the kernel returns proof_status VERIFIED_PROOF / REFUTED (kernel_error carries the kernel's exact complaint — use it to repair the proof and re-call) / UNDETERMINED (no toolchain / timeout / unresolvable import — honest, never fake). sorry/admit are REJECTED. mathlas never writes proofs, only checks them. Find declaration names first with search_formal_math. Args: statement, lean?, proof?.
Input Schema
| Name | Required | Description | Default |
|---|---|---|---|
| statement | Yes | the claim being checked; with `proof` it MUST be the Lean 4 proposition to prove, e.g. '∀ n : Nat, n + 0 = n' | |
| lean | No | Lean 4 snippet to kernel-check as-is, e.g. "example : 2 + 2 = 4 := rfl" (omit both this and `proof` and the verdict is an honest UNDETERMINED — statement text alone is not checkable) | |
| proof | No | YOUR Lean 4 proof of `statement` — a term ('rfl') or tactic block ('by\n intro n\n rfl'). Checked by the real kernel; on REFUTED, repair using `kernel_error` and re-call. sorry/admit holes are rejected. |
Output Schema
| Name | Required | Description | Default |
|---|---|---|---|
| statement | No | ||
| mode | No | 'proof_check' iff `proof` was supplied | |
| lean_provided | No | ||
| proof_provided | No | ||
| lean_available | Yes | ||
| tier | No | ||
| proof_status | No | proof mode only — the kernel's verdict on YOUR proof | |
| typechecks | Yes | ||
| applies | No | ||
| checked | Yes | true iff the Lean kernel actually ran and gave a verdict | |
| declaration | No | proof mode only — the exact declaration the kernel checked | |
| detail | No | ||
| kernel_error | No | proof mode, REFUTED only — the kernel's error verbatim; the repair-loop payload | |
| remediation | No | present iff not checked — exactly what unblocks a real kernel check | |
| note | No |