Tutorials

Five lessons, in order, from a fresh machine to an accepted proof and a running program.

Each tutorial builds on the one before it, and every step is something you run. By the end you will have a store holding proofs the Lean kernel has accepted, a theorem reused by its identity, and a program built from accepted code.

You need a checkout of lema-lang and a Linux x86_64 machine. Tutorials 2 to 5 also need the sandboxed runtime, which runs only where bubblewrap, systemd and a few libraries match the versions Lema pins; the first tutorial sets everything up and tells you whether your machine qualifies. If you want background first, read Build software like mathematics.

Set up a machine for Lema Install the pinned Rust and Lean from a lema-lang checkout, then find out whether this machine can run native calls.
Start a store and a server Create a store with the default axiom policy, run the server on a Unix socket, and ask it what the store holds.
Publish your first proof Publish a generic theorem and an implementation with its law, then read back what the store accepted.
Reuse a proof by identity Prove a new theorem by citing an accepted one through bindings, then point the same source at a second implementation.
Build and run a program Publish the SHA-256 specification and its entry points, then test, build and run them from an execution manifest.

Written against lema-lang at commit 5a94951, 17 Oct 2026.