Lean is a functional programming language that makes it easy to write correct
and maintainable code. You can also use Lean as an interactive theorem prover.
Lean programming primarily involves defining types and functions. This allows
your focus to remain on the problem domain and manipulating its data, rather
than the details of programming.
未完の日本語訳です．TPiL の日本語訳をお探しの方は https://aconite-ac.github.io/theorem_proving_in_lean4_ja/ へどうぞ
Defense grade Differential Privacy kernel and live network topology map designed for Critical Energy Infrastructure Protection (CIP) using Rust and Lean 4 constraints.
Evidence-gated frontier mathematics research workflow for DeepSeek Harness
Founder and CEO, SZL Holdings - governed AI infrastructure with inspectable source, runtime state, receipts, and proof boundaries.
SZL Living Anatomy — 3D navigable governed-AI organ substrate. Visualizes the 5 organs (reasoning cortex, trust gate, receipt bus, consensus, egress) powering a11oy + killinchu. Doctrine v11 LOCKED · 8 proven formulas · Λ = Conjecture 1.
Executable assurance kit for the seal mediation kernels: finite oracles and CLIs that turn the Lean 4 proofs into runnable, reviewer-checkable evidence.
Browser-runnable reference conformance checker for the SEAL mediation profile: a WASM L1 oracle that verifies seal decision receipts against the Lean-proven kernel.
Stephen Lutar evidence-first founder page: governed AI, Lean 4 proof boundaries, source/runtime receipts, and live SZL product links.
Lean4 library for Fixed point arithmetic
Openclaw platform designed for exploring, proving and searching proofs using the Lean 4 theorem prover
Static human-facing explorer for the Palomar database
Experimental tree-sitter parser for the Lean (4) Theorem Prover
Created by Leonardo de Moura
Released 2013