Lean 4 (4.31)

This assessment applies the coupling account — coupling as access to a shared resource, and the coupling floor [1], [2] — and the knowledge-embodiment theorem [3]; the language is assessed against its official reference [4].

1 Assessment

This page assesses Lean 4 in five parts: core coupling — what the language’s own constructs force; ecosystem coupling — what the surrounding platform, tooling, and community cost; engineering readiness — whether the artifact can be reproduced, verified, observed, worked in quickly, connected to other languages, and governed openly; the profile — the unscored facts a score cannot express; and the scoring detail — the mechanism marks and the arithmetic behind every score. A ✅ bullet marks a construct that helps. A ⚠️ or ❌ bullet marks a cost; the scoring model does not price every cost named here.

Core coupling 81/100 · Ecosystem coupling 65/100 · Engineering readiness 64/100

1.1 Core coupling

1.1.1 Type

  • ✅ Dependent types let a type name a value: Vector α n and Fin n carry the length in the type, so a length mismatch and an out-of-range index are rejected at elaboration
  • ✅ Propositions are types, so a proof is a term: The Curry–Howard correspondence puts a theorem and a program in one system, and the same kernel checks both
  • ✅ A structure type names its fields and their types: structure with typeclass fields gives a record whose construction is checked, and where supplies the values by name
  • ✅ Typeclass resolution is checked instance search: An instance is found by the declared class at compile time, so a missing instance is an elaboration error rather than a run-time lookup
  • ✅ Subtype couples a value to its proof: {x // p x} is a pair of a value and a proof that the predicate holds, so an invariant is carried by the term itself
  • ✅ unsafe marks the one escape from the logic: A declaration that bypasses the kernel must be named unsafe, so the boundary is visible in the source

1.1.2 Construction

  • ✅ Construction runs through the kernel, so an invariant cannot be skipped: A value of an inductive type is built by its constructors, and a term that does not fit the type fails elaboration
  • ✅ where puts the field values beside the type: An instance of a structure is written with named fields, so a reader does not count an argument list
  • ✅ macro and syntax extend the surface at the definition site: A notation for the domain is declared once and then used like a built-in
  • ✅ deriving generates the mechanical instances: Repr, BEq, Hashable, and Inhabited are produced by the elaborator, so a type does not repeat boilerplate
  • ✅ do notation builds the effectful value: Construction in IO, Option, or Except is written as a sequence of binds
  • ⚠️ Termination is an obligation on every definition: A recursive def must be shown to terminate structurally or by a decreasing measure, so a natural formulation of an algorithm can need a proof before it compiles

1.1.3 Memory

  • ✅ The compiler inserts the reference counting: Borrow inference decides which arguments are borrowed and which are owned, and emits the retain and release operations, so a pure definition never writes one
  • ✅ There is no tracing collector: A value is reclaimed when its last reference goes away, so there is no collection pause to plan around
  • ✅ A value of an inductive type is immutable: No term updates a field in place, so sharing is safe by construction
  • ⚠️ A reference cycle is not collected: A mutable reference cell (IO.Ref) whose value points back to the cell keeps its storage alive, because reference counting has no cycle detector
  • ⚠️ Allocation is not controllable from the source: The allocator is not a parameter and there is no placement control, so a program cannot choose where a value lives
  • ⚠️ A deeply shared structure still pays a count per reference: A persistent structure that shares a subtree is counted at every edge, and the compiler removes many but not all of those operations

1.1.4 Error

  • ✅ Option α and Except ε α are the error types: A partial function returns a value that states the failure, and do notation sequences the recovery path
  • ✅ A total function cannot fail by definition: In the pure fragment the type states that the function returns, and partial is required to opt out of that guarantee
  • ✅ Decidable turns a proposition into a branch that is total: if h : p then ... else ... computes from a proof of decidability, so the two branches cover the cases by construction
  • ✅ There are no exceptions in the logic: An error is a value in the return type, so a computation that can fail carries the failure in its signature rather than raising out of it
  • ⚠️ panic! and an IO failure leave the kernel’s guarantee: An abort at run time is not a term in the logic, and the type of the function does not mention it
  • ⚠️ Error-freedom is a theorem, not an automatic result: To state that a function never fails, you prove it; the compiler does not derive the property

1.1.5 Concurrency

  • ✅ The pure fragment has no shared mutable state: A mathematical term is a value with no location, so two proofs cannot race by construction
  • ✅ Task gives structured, joinable parallelism in IO: A task is a value that can be awaited, so a spawned computation is joined through its result
  • ⚠️ There is no concurrency construct in the language: Parallelism lives in the IO monad through Task and the promise cell, so a concurrent program is an IO program like any other
  • ⚠️ A promise carries a value between tasks and the program orders its use: Nothing in the type states when the value becomes available
  • ✅ The runtime owns the thread pool: The scheduler and its thread count are runtime settings, so the language does not expose a thread object
  • ⚠️ The kernel says nothing about a task’s behaviour: A theorem about a function does not constrain the parallel schedule that runs it

1.1.6 Platform

  • ❌ Lean 4 is the only implementation: The language is defined by its own elaborator and kernel, so there is no second independent compiler to test the specification against (P1)
  • ✅ The trusted kernel is small and portable: The elaborator is written in Lean and the kernel is a compact checker, so the language does not rest on a large run-time
  • ✅ @[extern] and @[export] make the foreign boundary a declaration: A call out to C is written and recorded, so the escape from the language is visible in the source
  • ✅ The output is C, so the target set is the C compiler’s: The compiler emits C and hands it to a C back end, so a Lean program runs where a C program runs
  • ⚠️ A native build needs a C toolchain and the Lean runtime: The build environment is part of the platform, and a deployed binary carries the runtime
  • ⚠️ The toolchain moves in nightly steps: A project pins its version in lean-toolchain, and a dependency may require a different one

1.1.7 Trade-offs (not coupling)

  • Proof work is a separate effort from programming: A def is not obliged to carry a proof, and requiring one is the author’s decision
  • The kernel is deliberately small and the tactics are not trusted: A tactic produces a term that the kernel rechecks, which is a decision about where trust sits
  • partial and unsafe are the intended escape hatches: A non-terminating or pointer-touching definition is expressible, at the cost of its guarantee
  • Typeclass search is a proof search with a cost: An instance can be ambiguous or expensive to find, and that is an elaboration property rather than a run-time coupling
  • The library is one large shared body: mathlib’s definitions belong to the community, so a development inherits its choices instead of buying a library
  • The audience is mathematics and verification: The adoption of the language follows from that, and it is a market fact rather than a mechanism of the language

1.2 Ecosystem coupling

1.2.1 Performance

  • ✅ The compiler emits C, and a native optimiser then compiles it: The generated C passes through a mature C back end, so the run-time cost benefits from that pipeline
  • ✅ Borrow inference removes most reference-count traffic: The compiler’s borrow analysis turns many retain and release pairs into nothing, so a pure functional definition stays close to imperative cost
  • ✅ @[inline] and @[specialize] remove an abstraction at the seam: A monomorphic specialisation of a polymorphic definition is generated on request
  • ✅ Compile-time evaluation removes run-time work: A proof discharged by decide or native_decide is computed while the project is built
  • ⚠️ Elaboration dominates the build time: Typeclass search, tactic execution, and proof checking are spent at compile time, so a large development builds slowly even when its binary is small
  • ⚠️ A count is not free on a shared structure: A persistent structure counted at each edge still pays for the sharing the compiler cannot prove away

1.2.2 Ecosystem

  • ❌ The package universe is small: Dependencies are resolved from git by lake, and the practical library set is mathlib, the core library, and a few support packages (Ec3)
  • ✅ lake is a standard build tool and dependency resolver: lakefile.lean or lakefile.toml declares a package, lake build builds it, and lake-manifest.json records the resolved revisions
  • ✅ The editor integration is first class: The Lean 4 server speaks LSP and the infoview shows the goal, the hypotheses, and the diagnostics beside the source
  • ✅ mathlib is one of the largest libraries of formalised mathematics: It is developed in the open and its continuous integration checks every proof
  • ⚠️ The community is academic and small: The centre of gravity is mathlib, the Zulip chat, and the university groups, and industrial use is rare
  • ⚠️ A project’s revision set is tight against the toolchain: mathlib tracks recent Lean releases, so a project that pins an older toolchain cannot use the current mathlib

1.2.3 Evolution

  • ✅ A project pins its toolchain and its dependency revisions: lean-toolchain names the version and lake-manifest.json names the commits, so a build is reproducible without a separate lock convention
  • ✅ Lean 4 is the stable line and its minor releases are backward compatible: A project on a pinned version is not moved by a release it did not take
  • ✅ The language and its libraries are open and publicly discussed: The request-for-comments archive and the community chat record why a feature changed
  • ⚠️ Lean 4 replaced Lean 3 with a different language: A Lean 3 development is a porting project, and the mathematical libraries moved with the new language
  • ⚠️ The ecosystem moves in nightly steps: A feature can land in a nightly build and reach a stable release later, so a dependency may require a version the project has not taken

1.2.4 Domain

  • ✅ Proof engineering and formalised mathematics are the native domain: theorem, by, simp, and mathlib are built for that work
  • ✅ Verified systems programming is supported: A verified algorithm compiles to C and ships as an ordinary binary, which is the growing use of the language
  • ✅ It is a general-purpose functional language beside the proof assistant: A def with no proof obligation is ordinary functional code
  • ❌ The domain lock-in is the point of the tool: The language expects a proof-carrying artifact, and a program that states no theorem gets little from the system (D1)
  • ⚠️ mathlib is a shared global body rather than a set of packages: A mathematical development is expected to build on its definitions, so the notation and the lemma names belong to the community
  • ⚠️ A formalisation is a research and maintenance commitment: A proof tracks the definitions it is about, so a change to one of them can invalidate a development

1.2.5 Learning

  • ❌ The curve is very steep: Dependent types, the elimination rules, and the elaborator’s inference model are new to a working programmer (L1)
  • ❌ Proof writing is a second skill on top of programming: Tactic scripts, the simp sets, and the explicit proof term are a subject of their own
  • ❌ The elaboration is not visible in the source: Why a by simp succeeded, or why an instance was not found, must be read from the goal state and the options (L3)
  • ✅ The infoview shows the goal and the hypotheses at the cursor: The state is displayed rather than inferred by the reader
  • ✅ The libraries supply the lemmas: An algebra or order fact is used without being reproved
  • ⚠️ The documentation trail is uneven: The reference manual is complete for the language, but much elaboration behaviour is documented in the source, and the community’s books are a growth area

1.2.6 Syntax

  • ✅ Term syntax reads like mathematics: ∀ x, P x → Q x, ∃, fun x => ..., and infix notation for the relations the library defines
  • ✅ Notation is declared and hygienic: notation, infix, and macro add a form where it is defined, so the surface can match the domain
  • ✅ do notation sequences effects as statements: let, if, and for inside do read like an imperative body over a monad
  • ✅ Pattern matching is checked for exhaustiveness: A missing constructor is a compile-time error, so a case is not forgotten
  • ⚠️ Layout is significant: do, by, and where blocks are delimited by indentation, so a re-indentation changes the parse
  • ⚠️ A macro can change what a line means: macro and elab rewrite the surface, so the reader must know the notation the library installed

1.2.7 Testing

  • ✅ #eval runs a term in the file: A definition can be evaluated and printed beside its proof, and #check reports its type
  • ✅ example and by decide state a checked claim inline: A decidable proposition is proved by evaluation, and an example block is a test the elaborator runs
  • ✅ lake test runs the project’s test executable: A test driver is declared in the package and run by the build tool
  • ✅ #print axioms reports the assumptions behind a theorem: A proof that used sorry or an extra axiom shows the dependency, so an unchecked step is discoverable
  • ⚠️ native_decide extends the trusted base: It closes a goal by evaluating compiled code, so the compiler and the runtime, not only the kernel, are relied on
  • ⚠️ An IO program is outside the logic: The behaviour of a program that reads a file or a socket is tested as an ordinary program rather than proved

1.2.8 Security

  • ✅ The kernel rechecks every proof term: A theorem that elaborates cannot be invalid, so a claimed property is a checked one
  • ✅ sorry is visible and reportable: The placeholder closes any goal with a warning, and #print axioms shows that it was used, so an unfinished proof is discoverable rather than hidden
  • ✅ unsafe names the escape from the logic: A declaration that bypasses the kernel is marked, so the boundary can be found in the source
  • ✅ No pointer type exists in the language surface: A term written without unsafe cannot express an address, so the memory-safety class of bugs is outside the pure fragment
  • ⚠️ The trusted base is wider than the kernel in a native binary: The runtime, the C compiler, and the runtime’s primitives are all in the path of a compiled program
  • ⚠️ There is no capability model: IO gives a program the authority of the operating system, and the sandbox is the operating system’s

1.3 Engineering readiness

1.3.1 Reproducibility

  • ❌ Builds are not byte-reproducible by default.

1.3.2 Supply chain

  • ⚠️ Published packages carry no signed provenance by default.
  • ⚠️ The package registry is a flat name space.

1.3.3 Observability

  • ⚠️ No stable tracing and metrics standard.
  • ⚠️ The standard library has no structured logging.

1.3.4 Feedback

  • ✅ No charged mechanism in this dimension.

1.3.5 Interop

  • ⚠️ No maintained portable target.

1.3.6 Governance

  • ✅ No charged mechanism in this dimension.

1.4 Profile

Unscored, and kept separate from every score on purpose. The profile records what a mechanism price cannot express: what a running program costs, how well a coding model and an agent work in the language, and whether a safety-critical path exists.

1.4.1 Energy and cost

What this axis asks: what does a running program cost in energy and time?

  • ✅ Compiles to native code: the fastest class in the language energy and time benchmarks [5], [6]. A causal re-analysis attributes the difference to execution time [7].

1.4.2 AI and agent readiness

What this axis asks: how well does a coding model and an agent work in this language?

  • ❌ Sparse training data: models write it unreliably [8].

1.4.3 Safety certification

What this axis asks: is there a certified or standards-qualified path to a safety-critical system?

  • ⚠️ No certified or standards-qualified path for safety-critical systems.

1.5 Scoring detail

1.5.1 Core coupling Dimensions

Dimension Mechanism Description Present Cost
Type T1 dynamic no static check — 0
T2 weak static — 0
T3 dynamic/duck dispatch — 0
T4 no sum types — 0
T5 no generics — 0
T6 no namespaces — 0
T7 type erasure/reflection — 0
T8 operator overloading — 0
T9 inheritance required for polymorphism — 0
T10 no null-safety — 0
T11 no module boundary — 0
T12 no effect tracking — 0
T13 async/sync colouring — 0
T14 unchecked foreign boundary ✅ −4
Type subtotal −4
Construction C1 global mutable state by default — 0
C2 no immutability by default — 0
C3 constructors coupled to allocation — 0
C4 no constructor/validation — 0
Construction subtotal 0
Memory M1 manual deallocation — 0
M2 GC non-deterministic pauses — 0
M3 no RAII — 0
M4 no ownership model — 0
Memory subtotal 0
Error Er1 no structured path — 0
Er2 unchecked exceptions only — 0
Er3 errors ignored/non-exhaustive — 0
Er4 no composable result type — 0
Error subtotal 0
Concurrency K1 GIL/no parallel — 0
K2 shared mutable state default — 0
K3 manual sync no race detection — 0
K4 no structured concurrency — 0
K5 no primitives — 0
Concurrency subtotal 0
Platform P1 cannot function outside one vendor/domain ✅ −15
P2 single-vendor but other uses — 0
P3 legacy/discontinued platform — 0
Platform subtotal −15

Core Dimensions score: 81/100 — total cost = −19 (per-dimension subtotals are capped at −15; an uncapped cost is shown in parentheses where the cap bites).

1.5.2 Ecosystem coupling Dimensions

Dimension Mechanism Description Present Cost
Performance R1 interpreted no AOT/JIT — 0
R2 GC pauses — 0
R3 JIT warmup — 0
Performance subtotal 0
Ecosystem Ec1 no package manager — 0
Ec2 fragmented tooling — 0
Ec3 small/niche/discontinued ✅ −8
Ec4 proprietary — 0
Ec5 platform-locked tooling — 0
Ec6 monoculture — 0
Ec7 legacy burden — 0
Ecosystem subtotal −8
Evolution V1 breaking changes — 0
V2 frozen — 0
V3 discontinued — 0
V4 glacial standards — 0
Evolution subtotal 0
Domain D1 domain/vendor lock-in ✅ −15
D2 poor domain fit — 0
D3 framework forces architecture — 0
Domain subtotal −15
Learning L1 steep ✅ −8
L2 large surface/multi-paradigm — 0
L3 sparse docs ✅ −4
Learning subtotal −12
Syntax S1 verbose — 0
S2 inconsistent — 0
S3 punctuation-heavy — 0
Syntax subtotal 0
Testing G1 weak tooling — 0
G2 poor debugging — 0
G3 runtime-only errors — 0
Testing subtotal 0
Security Q1 memory-unsafe — 0
Q2 dynamic/weak typing risk — 0
Q3 known vulnerability/injection — 0
Security subtotal 0

Meta Dimensions score: 65/100 — total cost = −35 (per-dimension subtotals are capped at −15; an uncapped cost is shown in parentheses where the cap bites).

1.5.3 Engineering readiness Dimensions

Dimension Mechanism Description Present Cost
Reproducibility Y1 build not reproducible ✅ −8
Y2 dependencies not pinned — 0
Reproducibility subtotal −8
Supply chain Y3 no signed provenance ✅ −8
Y4 registry without namespacing ✅ −4
Supply chain subtotal −12
Observability Y5 no stable tracing standard ✅ −8
Y6 no structured logging ✅ −4
Observability subtotal −12
Feedback Y7 slow build — 0
Y8 no fast in-editor analysis — 0
Feedback subtotal 0
Interop Y9 no foreign-function interface — 0
Y10 no portable target ✅ −4
Interop subtotal −4
Governance Y11 single-vendor governance — 0
Y12 closed specification — 0
Governance subtotal 0

Readiness Dimensions score: 64/100 — total cost = −36 (per-dimension subtotals are capped at −15; an uncapped cost is shown in parentheses where the cap bites).

Verdict: Lean 4’s design produces the highest core score here, because its constructs are separating by construction. Dependent types let a type state a property of a value, propositions-as-types puts the specification and the program in one term, and the kernel rechecks every proof, so an invalid claim does not elaborate. Reference counting with borrow inference keeps the memory story deterministic and out of the source. Main strengths: an exact fit to mathematics and verification, a small trusted kernel, and a first-class editor and library. Main weaknesses: the language has a single implementation, the library universe beyond mathlib is small, the toolchain moves in nightly steps, and the curve is among the steepest.

The formal development. The definitions, theorems, and proofs behind this page are published in:

All published papers

References

[1]
Y. Loth, “On the nature of coupling: All coupling as shared resource access.” Zenodo, Aug. 2026. doi: 10.5281/zenodo.21925122.
[2]
Y. Loth, “Coupling as a consequence of cohesion: Decomposition, the coupling floor, and domain-imposed coupling.” Zenodo, Aug. 2026. doi: 10.5281/zenodo.21925201.
[3]
Y. Loth, “On the nature of cohesion: Cohesion as correctness relative to a partitioning rule.” Zenodo, Jul. 2026. doi: 10.5281/zenodo.21703193.
[4]
Lean Focused Research Organization, “Lean language reference.” Lean, 2024. Available: https://lean-lang.org/doc/reference/latest/
[5]
R. Pereira et al., “Energy efficiency across programming languages: How do energy, time, and memory relate?” in Proceedings of the 10th ACM SIGPLAN international conference on software language engineering (SLE), 2017, pp. 256–267. doi: 10.1145/3136014.3136031.
[6]
R. Pereira et al., “Ranking programming languages by energy efficiency,” Science of Computer Programming, 2021, doi: 10.1016/j.scico.2021.102609.
[7]
N. van Kempen, H.-J. Kwon, D. T. Nguyen, and E. D. Berger, “It’s not easy being green: On the energy efficiency of programming languages,” in Proceedings of the 40th IEEE/ACM international conference on automated software engineering (ASE), 2025. doi: 10.1109/ASE63991.2025.00131.
[8]
S. Joel, J. J. Wu, and F. H. Fard, “A survey on LLM-based code generation for low-resource and domain-specific programming languages,” ACM Transactions on Software Engineering and Methodology, 2025, doi: 10.1145/3770084.