This site tracks the Lean 4 library in this repository: cryptographic primitives (LeanToolchain/Crypto), discrete linear algebra (LeanToolchain/Math), benchmarks, and the template-based Rust generator behind the rust/ crate.
| Topic | Where to read |
|---|---|
| Clone, build, first commands | Quick start |
| Lean, Elan, Rust setup | Installation |
Contributing rules, toolchain bumps, sorry policy |
Contributing (links to repo root) |
| SentinelOps vs GitHub Actions | CI overview |
What lake exe extract actually does |
Rust code generation |
| Lean coding style, proof tips | Style guide |
| Crypto API (Lean + generated Rust contract) | Crypto API |
| Vectors, matrices, norms (Lean) | Math API |
Vec design notes |
Vector implementation |
- Root README: README.md (overview, layout, security pointer).
- Security expectations: SECURITY.md.
From the repository root (with mkdocs and the Material theme installed, for example pip install mkdocs-material):
mkdocs build -f docs/mkdocs.ymlThe HTML output defaults to site/ relative to the current working directory unless overridden in your mkdocs setup.
The Lean release is pinned in lean-toolchain; mathlib is pinned in lakefile.lean and must stay compatible with that Lean version.
| Area | Status |
|---|---|
| Crypto (SHA-256 / HMAC) | Executable Lean definitions + structural lemmas; NIST/RFC vectors in Lean and Rust |
| Vectors / matrices | Dimension-indexed types; Bareiss det, Gaussian rank, Gauss–Jordan inverse; no general eigensolver |
| Real norms | mathlib ℝ norms; operator 2-norm exact for 1–2 columns, power iteration otherwise |
Rust rust/ |
Template-generated parallel implementations + Criterion benches; not proof extraction |