proof-polynomial

The proof-polynomial worked example.

Run it from sema/:

sema check examples/proof-polynomial
SEMA_STRICT=1 sema run examples/proof-polynomial
sema assure examples/proof-polynomial --grade silver

Source

src/main.sema

"""Exact, checked polynomial identities without pretending Sema is Lean.

`prove_identity(lhs, rhs)` reads the equation syntax directly, normalizes only
the bounded integer-polynomial fragment, and independently replays the emitted
certificate. Unsupported/domain-sensitive claims stay `unknown`; false claims
carry a concrete checked counterexample.
"""

assure silver

equation binomial_cube() -> Proof:
    return prove_identity(
        ("x" + "y")^3,
        "x"^3 + 3*"x"^2*"y" + 3*"x"*"y"^2 + "y"^3,
    )

equation false_square() -> Proof:
    return prove_identity("x"^2, "x")

equation domain_sensitive() -> Proof:
    return prove_identity("x" / "x", 1)

test "checked polynomial proof outcomes remain distinct":
    check binomial_cube().status == "proved"
    check binomial_cube().accepted
    check false_square().status == "disproved"
    check domain_sensitive().status == "unknown"

def main() -> str !{observe.record}:
    proved = binomial_cube()
    disproved = false_square()
    unknown = domain_sensitive()
    ensure proved.status == "proved" and proved.accepted
    ensure disproved.status == "disproved"
    ensure unknown.status == "unknown"
    log.info(
        "polynomial proof",
        proof_ref=proved.proof_ref,
        certificate=proved.certificate,
        counterexample=disproved.counterexample,
        unknown_reason=unknown.reason,
    )
    return proved.proof_ref

Reflected API

main

Exact, checked polynomial identities without pretending Sema is Lean.

prove_identity(lhs, rhs) reads the equation syntax directly, normalizes only the bounded integer-polynomial fragment, and independently replays the emitted certificate. Unsupported/domain-sensitive claims stay unknown; false claims carry a concrete checked counterexample.

def main

def main() -> str !{observe.record}

Returns str

Effects !{observe.record}