Documentation
How to use Lema, how it works, and exactly what each part does.
Lema is an experimental, theorem-native language. You state what must be true as a contract, agents write the implementation and its proofs in restricted Lean, and the server accepts them only after the pinned Lean 4.34.1 kernel replays every proof. Accepted objects are stored by identity, so a proof can be reused anywhere its statement is needed.
The docs are split by what you need at the moment. If you are new, start with the first tutorial. If you want the idea before the commands, read Build software like mathematics.
Lema is in development, and its repository is private for now. The tutorials and guides assume you have a checkout of lema-lang on a Linux x86_64 machine.
Tutorials
Lessons that take you from a fresh machine to your first accepted proof. Start here.
How-to guides
Steps for one job at a time, for when you already know what you want to do.
- Install the pinned Lean by hand
- Write a runtime configuration
- Create a store with a narrower axiom policy
- Move an alias safely
- Replace an implementation
- Name a set of objects with a bundle
- Set up a project reference
- Report on a change and merge two lines
- Build static inspection pages
- Build a native executable
- Release an artifact
- Build a capability app
- Re-check a store from scratch
- Recover from a HALTED latch
- Run the test suites
Reference
Commands, methods, formats and definitions, described exactly.
Explanation
Why Lema works the way it does, and where the project is going.
- Build software like mathematics
- Contracts, implementations and proofs
- Code stored by identity
- How acceptance works
- Programs that talk to the world
- Checked, tested and assumed
- Projects, history and review
- How programs reach the outside world
- Project status and roadmap
- Where the ideas come from
- Design decisions
Written against lema-lang at commit 5a94951, 17 Oct 2026.