# lean-theorems > The lean-theorems worked example. > The lean-theorems worked example. Run it from `sema/`: ```bash sema check examples/lean-theorems SEMA_STRICT=1 sema run examples/lean-theorems sema assure examples/lean-theorems --grade silver ``` ## Source ### `src/main.sema` ```sema """Native Lean 4 proof bridge worked example (LANGUAGE D109). A `theorem` declaration states a proposition in Sema's own equation notation. `sema check` elaborates every one of them to a single line of Lean 4 and validates that line against the adapter's verified fragment — no Lean process is spawned, so checking stays fast and hermetic. `lean.check` can then hand the same line to a real Lean 4.10.0 toolchain. WHAT A PASSING THEOREM ACTUALLY MEANS ------------------------------------- Elaborated and machine-checked by a *development* Lean toolchain. Nothing more. The adapter's ceiling on this path is `status = "CheckedUntrusted"` with `accepted = false`: a Lean 4.10.0 binary found on PATH read the source and exited clean with no diagnostics. Proof-grade `Verified` status additionally requires execution confinement, toolchain origin authentication, and an independently replayed certificate — all deliberately disabled today, so `lean.is_verified` is false for every result. These theorems are checked claims, not proofs. THE FRAGMENT'S LIMITS --------------------- `import` is forbidden, so there is no Mathlib and only Lean 4 core tactics are available: `omega` (linear integer arithmetic) and `decide` (closed decidable propositions). Consequently the elaborator REJECTS, with a span-accurate diagnostic rather than silently-wrong Lean: - existentials (`∃`, `∃!`) — `omega` cannot produce a witness; - nonlinear products (`x * y`) — at least one factor must be a literal; - powers, true division, decimals, `∞`, strings — the fragment is exact integer arithmetic over `Int`/`Nat` only; - sets, tensors, big operators, calculus — Lean core has no theory for them without `import`; - `bool` parameters — a Sema `bool` is a `Bool`, but a theorem body is a `Prop`, and no coercion between them exists here. Parameters must be `int` (→ `Int`) or `nat` (→ `Nat`), and the body must be exactly one proposition.""" assure gold # `x < y ⟹ x + 1 ≤ y` — the successor of a strictly smaller integer still fits. # Elaborates to `by omega`. theorem succ_bound(x: int, y: int): x < y ⟹ x + 1 ≤ y # Floor division and remainder reconstruct their dividend. `//` becomes Lean's # integer `/` and `%` its `%`; `omega` handles both against a literal divisor. theorem div_mod_reconstructs(n: int): 2 * (n // 2) + n % 2 = n # A `nat` parameter elaborates to Lean's `Nat`, where non-negativity is part of # the type rather than a hypothesis. theorem nat_is_non_negative(n: nat): n ≥ 0 # A `Range` binder domain is half-open, matching Sema's slice bounds: it adds # the hypotheses `0 ≤ i` and `i < n` inside the `∀`. theorem range_is_half_open(n: int): ∀ i ∈ 0..n : i < n # Strict positivity and `≥ 1` are the same claim over the integers — `⟺` maps # to Lean's `↔`. theorem positive_iff_at_least_one(x: int): x > 0 ⟺ x ≥ 1 # No parameters and no quantifiers, so the goal is closed and is discharged by # `by decide` instead of `by omega`. theorem product_is_exact(): 7 * 6 = 42 def instances(): """Concrete instances of the claims above, evaluated by Sema itself. A theorem is a universal claim about the arithmetic this program uses; these are the same facts at specific values, so the example stays runnable without a Lean toolchain present.""" return [ 3 + 1 <= 5, 2 * (7 // 2) + 7 % 2 == 7, all([i < 4 for i in range(0, 4)]), 7 * 6 == 42, ] test "every theorem instance holds at runtime": ensure all(instances()) == true def main(): ensure result == "6 theorems elaborate; 4 instances hold; status ceiling CheckedUntrusted" holding = len([held for held in instances() if held]) summary = f"6 theorems elaborate; {holding} instances hold; status ceiling CheckedUntrusted" print(summary) return summary ``` ## Reflected API # `main` Native Lean 4 proof bridge worked example (LANGUAGE D109). A `theorem` declaration states a proposition in Sema's own equation notation. `sema check` elaborates every one of them to a single line of Lean 4 and validates that line against the adapter's verified fragment — no Lean process is spawned, so checking stays fast and hermetic. `lean.check` can then hand the same line to a real Lean 4.10.0 toolchain. WHAT A PASSING THEOREM ACTUALLY MEANS ------------------------------------- Elaborated and machine-checked by a *development* Lean toolchain. Nothing more. The adapter's ceiling on this path is `status = "CheckedUntrusted"` with `accepted = false`: a Lean 4.10.0 binary found on PATH read the source and exited clean with no diagnostics. Proof-grade `Verified` status additionally requires execution confinement, toolchain origin authentication, and an independently replayed certificate — all deliberately disabled today, so `lean.is_verified` is false for every result. These theorems are checked claims, not proofs. THE FRAGMENT'S LIMITS --------------------- `import` is forbidden, so there is no Mathlib and only Lean 4 core tactics are available: `omega` (linear integer arithmetic) and `decide` (closed decidable propositions). Consequently the elaborator REJECTS, with a span-accurate diagnostic rather than silently-wrong Lean: - existentials (`∃`, `∃!`) — `omega` cannot produce a witness; - nonlinear products (`x * y`) — at least one factor must be a literal; - powers, true division, decimals, `∞`, strings — the fragment is exact integer arithmetic over `Int`/`Nat` only; - sets, tensors, big operators, calculus — Lean core has no theory for them without `import`; - `bool` parameters — a Sema `bool` is a `Bool`, but a theorem body is a `Prop`, and no coercion between them exists here. Parameters must be `int` (→ `Int`) or `nat` (→ `Nat`), and the body must be exactly one proposition. # `def instances` ```sema def instances() ``` Concrete instances of the claims above, evaluated by Sema itself. A theorem is a universal claim about the arithmetic this program uses; these are the same facts at specific values, so the example stays runnable without a Lean toolchain present. # `def main` ```sema def main() ```