lean-theorems

The lean-theorems worked example.

Run it from sema/:

sema check examples/lean-theorems
SEMA_STRICT=1 sema run examples/lean-theorems
sema assure examples/lean-theorems --grade silver

Source

src/main.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

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

def main()