Skip to content

ghuntley/lean5

BranchesTags
 
 

Repository files navigation

Lean5

Pure Rust theorem-proving infrastructure for AI-driven verification.

What is Lean5?

Lean5 is a from-scratch Rust theorem-proving stack built for Lean 4 compatibility, kernel-backed checking, and AI-driven verification workflows. It implements the same core dependent type theory family as Lean 4, but the practical Lean 4 replacement surface is still phase-gated work: parser, elaborator, tactic, Lake, LSP, compiler, and native-library parity are tracked by the roadmap and verification gates below.

If you want to:

  • Verify proofs programmatically — Lean5 is a Rust library you can call directly, no subprocess or REPL needed.
  • Build an AI proof search system — historical benchmark snapshots have shown 1M ops/sec batch throughput; current public performance claims must be backed by fresh benchmark artifacts.
  • Type-check Lean-style code from Rust — broad Lean 4 syntax coverage, .olean import for selected Init/Std/Mathlib lanes, and a growing tactic surface with explicit trust reporting.
  • Verify C or Rust programs — built-in ACSL/separation logic for C, VIR/NLL/stacked-borrows for Rust.
  • Run an SMT-backed tactic engine — integrated z4 solver with proof reconstruction.
  • Search the world's formal math — the Omega Library unifies 3.25M declarations from 68 proof systems (Lean 4, Coq, Metamath, HOL, Mizar, Agda, Isabelle, ...) with explicit trust tracking.

If you want interactive theorem proving for humans, use Lean 4 — it has a mature editor experience and large community. Lean5 is infrastructure, not an IDE.

Public Launch Surface

The launch-facing public contract is intentionally narrower than the full research workspace:

  • lean5 check is the primary demo path for kernel-backed checking and trust reporting.
  • lean5 features, lean5 help, and docs/cli/index.md are the generated CLI surface.
  • docs/RELEASE_READINESS.md names the current release-readiness smoke gate.
  • docs/PUBLIC_DEMO.md records the reproducible public demo commands:
cargo run --locked -p lean5 --bin lean5 -- check demos/public/kernel_check_success.lean
cargo run --locked -p lean5 --bin lean5 -- check demos/public/kernel_check_reject_sorry.lean

demo contract:

Lean5 public demo
build: ok
accept: demos/public/kernel_check_success.lean
  expected: Checked 4 declarations; 4 passed, 0 failed
  observed: ok
trust-reject: demos/public/kernel_check_reject_sorry.lean
  expected: explicit sorry rejected
  observed: rejected with sorry axioms: 1
result: PASS

The reproducible public path is split by claim type:

  • Demo and trust smoke: run the published demo commands above; see docs/PUBLIC_DEMO.md.
  • Benchmark claims: validate fresh benchmark artifacts and cite docs/BENCHMARKS.md.
  • Broader trust/correctness status: check docs/VERIFICATION_AUDIT.md before expanding public claims beyond the demo trust-reject lane.

Numeric claims in this README are either sourced from cited release metadata or marked as historical snapshots.

Cargo.lock is tracked. Public build, test, and run commands in this repository use --locked so fresh clones fail fast instead of silently resolving a different dependency graph.

Authorship, Credits, and TLA+

Lean5 is authored by Andrew Yates.

lean5-tla depends on the public tla-core crate from the public andrewdyates/tla2 repository. The names differ because tla2 is the repository/workspace name, while tla-core is the reusable library crate inside it that Lean5 imports. Lean5 uses that shared public TLA+ AST and TLAPS obligation model instead of maintaining a second incompatible TLA+ front end.

Lean5 is built against and explicitly credits the Lean 4 ecosystem:

Installation and Usage

As a Rust library (recommended)

Add Lean5 to your project:

# Cargo.toml
[dependencies]
lean5 = { git = "https://github.com/andrewdyates/lean5" }

Basic type checking:

use lean5::prelude::*;

fn main() -> Result<(), Box<dyn std::error::Error>> {
    let env = Environment::with_prelude();
    let mut tc = env.type_checker();

    // Type check: Nat.add 1 2
    let expr = tc.app(tc.const_("Nat.add"), [tc.lit(1), tc.lit(2)]);
    let ty = tc.infer_type(&expr)?;  // historical microbenchmark: ~500ns

    assert_eq!(ty, tc.const_("Nat"));
    Ok(())
}

Load Mathlib:

let env = Environment::with_mathlib()?;

Batch verification (AI proof search)

The primary use case — verify many candidates, keep the first valid proof:

use lean5::prelude::*;

let env = Environment::with_prelude();
let verifier = BatchVerifier::new(&env);
let candidates: Vec<Expr> = generate_candidates();

// Find the first valid proof (common LLM search pattern)
if let Some((expr, ty)) = verifier.find_first_valid(candidates.into_iter()) {
    println!("Proved: {:?}", ty);
}

// Or search in parallel with early termination
if let Some((expr, ty)) = verifier.find_first_valid_parallel(&candidates) {
    println!("Proved in parallel: {:?}", ty);
}

JSON-RPC server

For non-Rust clients, Lean5 exposes a JSON-RPC server over TCP or WebSocket:

# Build and start the server
cargo build --locked --release
cargo run --locked -p lean5 -- server --port 8080              # TCP
cargo run --locked -p lean5 -- server --port 8081 --websocket  # WebSocket
# Check a definition
echo '{"jsonrpc":"2.0","method":"check","params":{"code":"def f (n:Nat) := n+1"},"id":1}' \
  | nc localhost 8080
{"jsonrpc":"2.0","result":{"valid":true,"type_":"Nat -> Nat"},"id":1}

The method registry covers type checking, automated proving, proof-state management, certificate operations, C verification, and environment management. See JSON_RPC_API.md.

From the command line

cargo build --locked --release
CARGO_ALLOW_FULL_SUITE=1 cargo test --locked --message-format=short -j 1       # run the test suite (38K+ tests)

The unified lean5 binary exposes every feature through a single entrypoint. Subcommands include: check, eval, verify, auto, server, repl, lake, fold, commit, cert, kernel, bench, promote, discover, tlaps, features, help, omega, olean, lsp, compile, and sorry-trace. Specialized binaries ship alongside it: omega, omega_convert, omega_shard, omega_try, and lean5_depgraph.

Discover what is available with:

lean5 features                         # flat index of every registered feature
lean5 features --category verification # filter by category
lean5 features --stability experimental # show experimental surfaces such as sorry-trace
lean5 features --stability v1          # filter by stability level
lean5 features --search sorry          # free-text search over paths and summaries
lean5 features --json                  # JSON output for tooling
lean5 help                             # print the help index pointer
lean5 help check                       # render the Markdown help for `lean5 check`
lean5 help sorry-trace                 # render the Markdown help for `lean5 sorry-trace`

AI Factory Quick Start

Lean5 now exposes a Rust-owned factory surface for agents that need to coordinate proof work, inspect theorem changes, and keep merge evidence machine-readable. Start with the guide:

lean5 factory guide
lean5 factory guide --json

The current agent loop is:

  1. Align the checkout with git pull --ff-only.
  2. Inspect release/tool health with lean5 factory status --json.
  3. Build a declaration/trust inventory with lean5 factory decl-index --root . --json.
  4. Gate candidate Lean-source merges with lean5 factory merge-check --base main --candidate HEAD --json.
  5. Serialize clean candidate refs through lean5 factory queue push, lean5 factory queue status --json, and lean5 factory queue process-next --verify-cmd '<cmd>' --json.

For proof agents, pair the factory commands with:

  • lean5 server for JSON-RPC proof-state, tactic, certificate, and batch verification calls;
  • lean5 auto premise for the current goal-shaped premise shortlist;
  • cert_simp and cert_omega for proof-carrying simplification and arithmetic normalization;
  • docs/reference/proof-state-serialization.md for the current proof-state wire contract;
  • planned v2 proof-state/theorem-search API work tracked from the private source workspace until the public contract is stable.

The critical rule is that search output is advice, not proof. Treat a branch as proved only after kernel verification and a clean trust_summary.

Interactive REPL

For quick experimentation, lean5 repl launches an interactive session backed by a persistent Environment::with_prelude(). It uses rustyline for line editing and history, and supports a handful of meta-commands:

lean5 repl
Command Effect
:type <expr> Infer and print the type of an expression
:load <file> Type-check a .lean source file into the current session
:env [substr] List environment constants, optionally filtered by a substring
:help Show available meta-commands
:quit Exit the REPL

Bare input is type-checked against the live environment. History persists across sessions under $XDG_CACHE_HOME/lean5/repl_history (falling back to the platform cache directory). This is a programmer's REPL — for a full interactive proof-authoring experience, use Lean 4.

How It Works

Lean5 implements the Calculus of Inductive Constructions (CIC) — the same type theory as Lean 4 and Coq. The trusted core is the kernel, which checks that proof terms have the correct types. Everything else (parsing, elaboration, tactics, automation) builds proof terms that the kernel verifies.

Source code (Lean 4 syntax)
       │
       ▼
   Parser ──────────────── Lean 4 surface syntax → AST
       │
       ▼
  Elaborator ──────────── Type inference, implicit arguments, coercions
       │
       ▼
  Tactic Engine ────────── Lean-style tactics (simp, ring, omega, linarith, aesop, ...)
       │                   ├── SMT bridge (z4 solver with proof reconstruction)
       │                   └── Superposition prover, premise selection
       ▼
   Kernel ─────────────── Trusted type checker (historical sort-check snapshot: ~36-47ns)
       │
       ▼
  Certificate ─────────── Verifiable proof artifact (~410-560ns)

Why Rust?

Lean 4 (C++) Lean5 historical snapshot
Type check latency ~1ms 36-47ns
Batch throughput — 1M ops/sec
Primary API REPL / LSP Rust library (+ JSON-RPC)
Memory safety Manual Ownership + #![forbid(unsafe_code)] in kernel
C verification No Yes (ACSL, separation logic)
Rust verification No Yes (VIR, NLL, stacked borrows)

Lean 4 does not publish kernel-level microbenchmarks; estimate based on typical proof-checking latency. Treat these as historical engineering numbers unless backed by current benchmark artifacts. See BENCHMARKS.md.

Features

Lean 4 Compatibility

Lean5 can parse and type-check a substantial Lean 4-style subset, but this is compatibility infrastructure, not a full Lean 4 replacement claim:

  • Surface syntax: broad FATE-X and Lean 4 corpus coverage, with tracked parse-only and elaboration lanes instead of an unqualified parity guarantee.
  • Type checker: cross-validated against lean4lean-scoped kernel cases.
  • .olean import: Init and Std lanes plus Mathlib import/search support with explicit stub fallback where needed; see MATHLIB_STUBS.md.
  • Tactics: Lean-style tactic engine covering core automation paths such as simp, ring, linarith, omega, nlinarith, norm_num, aesop, and decide, with trust markers surfaced by lean5 check.
  • Mathlib elaboration: tracked as an active compatibility metric, not a complete native Mathlib replacement.

C Verification

Verify C functions with ACSL specifications and separation logic contracts:

/*@ requires n >= 0;
    ensures \result >= 0; */
int abs(int n) {
    return n < 0 ? -n : n;
}

8 worked examples in crates/lean5-c-sem/src/examples.rs: abs, swap, array_sum, constant_time_compare, xor_cipher, safe_array_access, memcpy, and binary_search.

Rust Verification

Source ingestion, VIR lowering, NLL borrow checking, and stacked-borrows evaluation. Worked examples in crates/lean5-rust-sem/src/examples.rs.

Automation

  • SMT integration via z4 solver with Alethe proof reconstruction
  • Superposition prover for first-order reasoning
  • Premise selection for automated lemma discovery
  • ATP/TPTP interface for external provers
  • Proof-factory queue via lean5 factory queue ..., backed by data/proof_queue.json for tier-ordered, dependency-aware dispatcher use.

Proof Infrastructure

Tools for constructing, searching, and auditing kernel-verified proofs:

Gamma-crown proof status (2026-04-20): the Lean5-Native .omega shard (cargo run --locked -p lean5-omega --bin omega_shard -- build-native <out-dir>) exports 42 theorems whose transitive axiom closure is ⊆ FOUNDATIONAL_AXIOMS (propext, Quot.sound, Classical.choice, Eq built-ins, plus standard Rat/Nat/Fin primitives documented inline in axiom_audit.rs). Per #3554, sorryAx was moved to a separate TRUST_MARKERS predicate so the classifier now fails closed on any transitive trust-envelope reference. Trajectory: 21 (pre-demasquerade) → 15 (after 2026-04-19 MASQUERADE sweep demoted fake proofs back to Declaration::Axiom) → 28 (2026-04-19 T4 unlock: Rat.max/Rat.min + _def equations promoted to foundational) → 47 (Tier A Rat lemmas + IntervalArith abs/div/monotone/pow/recip/sqrt/width landed) → 42 (2026-04-20 wave-9 Branch A demasquerade sweep: C006.blockwise_nat_induction, C006.compose, C006.monolithic_crown, C006.blockwise_equals_monolithic, Block.blockwise_crown_equiv, C010.both_compute_exact_affine, T72.cert_composition_trust, LayerNorm.zonotope_generators_reset all demoted from Theorem back to Axiom/Opaque because their proofs collapsed over argument-discarding reducible carriers; net shard dropped by 5 but axiom-dependent reject rose 5→25, making trust gaps honest). Honest breakdown of the 42: 11 foundational utility (Eq/Iff/congr/congrArg/congrFun/congrFun'), 5 Tier A Rat lemmas (Rat.min_zero_zero, Rat.le_refl_zero, Rat.zero_eq_max, Rat.zero_eq_min, Rat.max_eq_min), 7 IntervalArith theorems (abs, div, monotone, pow, recip, sqrt, width_monotone — real content), 3 Phase-3 compose-scaffolding (blockwise_crown_equiv_faithful, compose_faithful_succ_unfold, compose_faithful_zero_eq_input — real but partial), 4 ReLU primitives, and Nat/Rat building blocks (Nat.le_trans, Rat.inv_zero, Rat.mul_sub, Rat.sub_self, Rat.add_comm, Rat.add_assoc, Rat.mul_assoc). Headline claims remain axiomatized. T60 (monolithic CROWN soundness), full C004 (CROWN-IBP equivalence), full C006 (blockwise CROWN) are Declaration::Axiom. T20/T21 were demoted per #3509; C006.compose/monolithic_crown/blockwise_nat_induction/blockwise_equals_monolithic per wave-9 Branch A 2026-04-20. Open remediation issues: #3490 (Batch 1+: ibp_width_zero general-case), #3491, #3492, #3493, #3494 (headline remediation has a private design record, estimated 3-4 agent sessions). Epic #3551 tracks the remaining axiom-dependent rejects (Wave-11 gamma-crown triage: 29 Tier A, 19 Tier B, 12 Tier C, 15 Tier D reclassify-only). Honest scope: 15-28 further agent sessions to land substantive NN-verify theorems beyond the current real-content set.

Omega Library — Universal Verified Mathematics

The Omega Library imports, verifies, and indexes theorems from the world's formal proof systems into a single searchable archive. It also exports lean5-proved theorems back to .omega shards, closing the Math-to-Omega-to-Math loop.

Current release: omega-v0.9.0 (2026-04-01) — 3,254,463 declarations converted from 68 source systems into 107 .omega shards. A broader census tracks 30,049,434 declarations across 238 scanned repositories (see OMEGA_LIBRARIES.md).

The .omega shard files are not checked into the git tree. Release download tooling only accepts GitHub Releases that publish a compatible omega-library-v*.tar.zst archive with omega-manifest.json checksums. The omega-v0.9.0 release records the canonical public counts above, but it does not include a downloader-compatible archive; build shards from source until a compatible Omega release is published.

Source Systems Declarations Verified
Metamath (set.mm, iset.mm, nf.mm, ql.mm, hol.mm) 70,042 theorems RPN-verified, 0 failures
Lean 4 (Init, Std, Lean, Lake) 100K+ constants Kernel type-checked
Coq (UniMath, MathComp, Flocq, CompCert) varies CIC → kernel Expr
HOL Light, HOL4 — Type/term embedding
Mizar MML — FOL → DTT translation
Agda, Idris 2, F* — Structured parse
Isabelle AFP, OpenTheory, TPTP, SMT-LIB, TLA+, ... — Structured importers

Pipeline highlights:

  • Math-to-Omega-to-Math loop — export lean5-proved theorems to .omega shards via omega export
  • Keyword search — tag constants with research keywords, search by tag via omega find --tag
  • Similar theorem discovery — find related theorems across systems by name, domain, and type fingerprint
  • arXiv formalization — bridge arXiv papers to .omega shards with paper ID tagging
  • Cross-system equivalence graph — discover equivalent theorems across proof systems
  • Metamath RPN verification — 70,042 theorems re-checked end-to-end with 0 failures
  • OpenTheory import — 99.6% success rate over the standard corpus
# Download a pre-built Omega library only from a release that includes
# a compatible omega-library-v*.tar.zst asset plus omega-manifest.json.

# Convert all sources to .omega shards
cargo run --locked -p lean5-omega --release --bin omega_convert -- all /tmp/omega-data

# Verify shard integrity (blake3 checksums)
cargo run --locked -p lean5-omega --release --bin omega_shard -- verify data/omega-shards/

# Search for theorems by name, tag, or similarity
cargo run --locked -p lean5-omega --release --bin omega -- find "Nat.add_comm"
cargo run --locked -p lean5-omega --release --bin omega -- find --tag "algebra"

# Export lean5-native theorems to omega shards
cargo run --locked -p lean5-omega --release --bin omega -- export --source lean5-native

# Build the lean5-native shard
cargo run --locked -p lean5-omega --release --bin omega_shard -- build-native /tmp/native-shard

Each .omega shard is a binary format containing: zstd-compressed string tables, 16-byte expression arenas, 32-byte constant headers with per-theorem trust level, axiom profile, and content domain classification. Trust gates prevent contamination between trust levels (KernelVerified, ProofCarrying, Axiomatized, External).

Full census: data/OMEGA_LIBRARIES.md (238 repositories scanned). Import tier classification: data/OMEGA_KERNEL_COMPATIBILITY.md.

Self-Verification

The kernel includes a formal specification (183 definitions), 68 proof witnesses, a ~2,900-line micro-checker, and cross-validation against lean4lean. Proof execution is paused pending constructive TypePreservation. The live TypePreservation trust frontier is 1 structural HelperAxiom — church_rosser_whnf (deferred to #2859) — pinned by TYPE_PRESERVATION_LEAVES in crates/lean5-verify/src/spec/core_spec/type_preservation_chain_status_tests.rs. def_eq_to_eq has already been demoted off the frontier, so the historical 7-lemma picture is stale: the remaining pending chain now collapses to the single church_rosser_whnf leaf.

Architecture

Lean5 is organized as a Cargo workspace with 27 crates:

lean5/
 crates/
   lean5/              ← Rust API entry point (re-exports kernel + loaders)
   lean5-lib/          ← Shared library surface consumed by binaries
   lean5-kernel/       ← Trusted type checker core
   lean5-parser/       ← Lean 4 syntax parser
   lean5-elab/         ← Elaboration + Lean-style tactic engine
   lean5-auto/         ← SMT, superposition, ATP, premise selection
   lean5-compiler/     ← Compiler IR (L5CNF / L5IR)
   lean5-server/       ← JSON-RPC server (TCP + WebSocket)
   lean5-olean/        ← .olean file import
   lean5-c-sem/        ← C verification (CompCert model, ACSL)
   lean5-rust-sem/     ← Rust verification (VIR, NLL, stacked borrows)
   lean5-verify/       ← Self-verification infrastructure
   lean5-omega/        ← Omega Library: 68-system math import/export, .omega shards, search
   lean5-tla/          ← TLA+ encoding and TLAPS backend
   lean5-cli/          ← Command-line interface (unified `lean5` binary)
   lean5-features/     ← Feature registry powering `lean5 features` / `lean5 help`
   lean5-discovery/    ← Cross-repo feature discovery and indexing
   lean5-runtime/      ← Runtime (reference counting, IO)
   lean5-lsp/          ← Language Server Protocol
   lean5-lake/         ← Build system (Lake compatibility)
   lean5-fold/         ← Nova-style folding for proof compression
   lean5-commit/       ← Polynomial commitment schemes (KZG/IPA)
   lean5-gpu/          ← GPU acceleration (wgpu)
   lean5-macro/        ← Procedural macros
   lean5-sys/          ← FFI bindings
   lean5-coq-import/   ← Coq proof import
   lean5-tlaps-bench/  ← TLAPS benchmarks

The kernel (lean5-kernel) is the trusted core — it uses #![forbid(unsafe_code)], has zero unwrap() or unimplemented!() in production paths, and all recursive functions use stack-safe wrappers.

Historical Performance Snapshot

The numbers below are historical local snapshots measured on Apple M4 Max, 128GB. Treat them as engineering context, not current launch claims, unless they are backed by fresh publication artifacts under the benchmark contract in BENCHMARKS.md.

Operation Latency
is_def_eq (identical) 2.8ns
whnf (delta unfold) 29ns
whnf (beta simple) 40ns
infer_type (Sort) 36-47ns
is_def_eq (beta reduce) 163ns
infer_type (app) 487ns
Certificate verify 410-560ns
JSON-RPC check 24-28µs
Batch throughput 1M ops/sec

Project Status

Workspace manifest version is v1.2.0. The current public release is v1.2.0; prior tagged releases include v1.1.0, v1.0.0 (core, 2026-03-25), and omega-v0.9.0 (omega shards, 2026-04-01). Current generated workspace metric: 1,788,080 lines of Rust. 38,972 tests. The workspace has 27 crates.

Current public release-readiness status lives in docs/RELEASE_READINESS.md. The generated CLI reference lives under docs/cli/index.md and lean5 help.

Component Status Notes
Kernel (type checker) 459K 8115
Parser (Lean 4 syntax) 27K 734
Elaborator 366K 9427
Compiler 148K 4477
Automation (SMT/ATP) 129K 2212
Server (JSON-RPC) 34K 192
.olean Import 38K 520
Runtime Production Reference counting, IO
C Verification 21K 307
TLA+ Usable TLAPS backend
Omega Library Released (omega-v0.9.0) 3,254,463 declarations, 68 source systems, 107 shards
Rust Semantics 83K 1379
Self-Verification 231K 6351

Counts generated from release metadata (updated 2026-04-25).

Backlog Snapshot

GitHub backlog totals are volatile and are intentionally not frozen in this README. Reproduce the current open-issue snapshot with:

gh issue list --state open --limit 500 \
  --json number,labels \
  --jq '{
    open: length,
    labels: (map(.labels[].name)
      | group_by(.)
      | map({label: .[0], count: length})
      | map(select(.label as $l | [
          "P1", "P2", "P3", "urgent", "blocked", "in-progress",
          "local-maximum", "using-lean5", "zone:proof-corpus",
          "building-lean5", "zone:automation", "zone:trust-core",
          "zone:tooling", "zone:frontend"
        ] | index($l))))
  }'

Launch issue state below was checked on 2026-04-25. Re-check with GitHub before tagging or publishing release notes.

Detailed engineering sequencing remains in design documents, but the public-facing launch blockers are tracked through GitHub issues and release readiness docs. Completed and closure-ready launch evidence lanes are:

  • #3669 is closed for the public docs drift audit; keep the release docs gate in docs/RELEASE_READINESS.md as the evidence surface.
  • #3670 is closed for the reproducible public demo path; the evidence contract is docs/PUBLIC_DEMO.md.
  • #3672 is closed for the public benchmark suite and freshness policy; the evidence contract is docs/BENCHMARKS.md, with launch gating in docs/RELEASE_READINESS.md.
  • #3498 is closure-ready for the old orphan-binary blocker: the remaining user-facing CLI paths are absorbed or indexed, operator-only binaries are surfaced through OperatorTools, and verify_mathlib is no longer shipped.

Active platform priorities and launch blockers are:

  • #3656: close the remaining bridge-dependent Rat theorem rollback before trusting more native-shard promotions.
  • #3646, #3640: widen the MASQUERADE detector and refresh data/axiom_audit.json so published trust counts stay honest.
  • #2623: fix broken URLs that block OSS publication.
  • #3671: finish the top-level release readiness gate in docs/RELEASE_READINESS.md.
  • #464, #2859: continue the TypePreservation chain once the trust and launch blockers above are contained.

Recently closed lanes to keep out of blocker lists:

  • #3654: closed the unsound Rat.mk_eq_mk_of_cross_eq bridge incident.
  • #3657: closed the bridge-dependent closure drift guard.
  • #3428: closed the merge-queue sequencer work.

Documentation

Document Description
DESIGN.md Architecture, API reference, full specification
BENCHMARKS.md Reproducible benchmark methodology
PUBLIC_DEMO.md Current public demo status and required trust behavior
RELEASE_READINESS.md Top-level release-readiness smoke gate
docs/cli/index.md Generated CLI command reference
JSON_RPC_API.md JSON-RPC method reference
PHILOSOPHY.md Design principles
VERIFICATION_AUDIT.md Current correctness and trust-gap register
ACKNOWLEDGMENTS.md Authorship, upstream credits, and citation entry points
CITATION.cff Preferred software citation for Lean5
EXTERNAL_CERTIFICATES.md External certificate schemas
EXTERNAL_CONSUMERS.md Integration contracts for downstream repos
LEAN4_REFERENCE_MAP.md Lean 4 source anchors used for parity work
LEAN4LEAN_COVERAGE.md lean4lean theorem/test coverage matrix
OMEGA_LIBRARIES.md Omega Library full census (238 systems, 30M+ declarations)
OMEGA_KERNEL_COMPATIBILITY.md Import tier classification and gap analysis
OMEGA_PROVENANCE.md Provenance and trust tracking for imported theorems

Building from Source (Installation)

Requirements: Rust 1.75+ (nightly recommended for best performance).

git clone https://github.com/andrewdyates/lean5
cd lean5
cargo build --locked --release
CARGO_ALLOW_FULL_SUITE=1 cargo test --locked --message-format=short -j 1

The workspace compiles as a single cargo build --locked with no external C/C++ dependencies.

License

Apache-2.0. See LICENSE.

Copyright 2026 Dropbox

About

lean4 ported to Rust for AI self-coding in real time

Resources

Readme

License

View license

Security policy

Security policy
Activity

Stars

2 stars

Watchers

0 watching

Forks

0 forks
Report repository

Releases

No releases published

Packages

 
 
 

Contributors

Languages

  • Rust 70.0%
  • Lean 27.6%
  • Python 1.6%
  • Shell 0.5%
  • TLA 0.2%
  • C 0.1%