Generated by
sema docfrom the compiler’s authoritative native-signature registry.
lean (native adapter)
Section titled “lean (native adapter)”Bounded Lean 4.10.0 kernel adapter — bring it in with import lean; calls require proc.run (LANGUAGE D109).
formal
Section titled “formal”lean.check(source) -> LeanCheckResult
Section titled “lean.check(source) -> LeanCheckResult”Check an allowlisted named-theorem fragment with Lean 4.10.0; examples are rejected because Lean does not persist them as replayable proof roots. PATH execution is explicitly CheckedUntrusted, pinned execution is currently unavailable on every platform, and AuthenticatedConfined/Verified stay reserved until the isolated-runner qualification contract is satisfied.
- domain: one or more complete unindented LF-only named theorem declarations in UTF-8 Lean source up to 256 KiB; ordinary strings only; no example/sorry/axiom/notation/unsafe/metaprogram/environment/native-evaluation commands; exact Lean 4.10.0; zero diagnostics; bounded output and 15 s wall time; PATH checks stay CheckedUntrusted; every pinned root-owned toolchain fails closed to Unavailable before execution until a deny-default isolated runner is qualified
- shape: scalar
- returns:
LeanCheckResult - effects:
proc.run - example:
lean.check("theorem sema_registry_ok : True := True.intro")
lean.is_verified(evidence) -> bool
Section titled “lean.is_verified(evidence) -> bool”Return true only for origin-authenticated, immutable, kernel-checked, process-clean, confined, certificate-replayed Verified evidence; false for every current adapter result because pinned execution and both authenticated statuses remain unavailable.
- domain: an authenticated in-process LeanCheckResult; copied fields, JSON, dictionaries, and nominal lookalikes return false
- shape: scalar
- returns:
bool - example:
lean.is_verified(None)