# lean > Native bounded Lean theorem-prover adapter operations. > Generated by `sema doc` from the compiler's authoritative native-signature registry. # lean (native adapter) Bounded Lean 4.10.0 kernel adapter — bring it in with `import lean`; calls require `proc.run` (LANGUAGE D109). # formal ## `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` 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)`