# Bend2 vs Lean

Last updated 2026-08-05. Canonical: https://bend2.dev/notes/bend2-vs-lean/

Bend2 and Lean will be compared endlessly because both have dependent types, and the comparison
is mostly a category error. Lean is a proof assistant that happens to be a
serious programming language. Bend2, per its creator's public statements, is a programming
language that happens to prove things, with execution on a massively parallel runtime as the
point. They meet at the type theory and diverge at everything downstream of it.

## What Lean is

Lean 4, the mature side of the Bend2 comparison, is a
[theorem prover and programming language](https://github.com/leanprover/lean4) developed under
Leonardo de Moura, stewarded since 2023 by the Lean FRO, Apache 2 licensed, with
its own [system description](https://lean-lang.org/papers/lean4.pdf). The language is real:
Lean 4 is self-hosted, compiles through C, and runs on a reference-counted runtime with
task-level concurrency that the compiler itself exercises. But Lean's center of mass is
[mathlib](https://github.com/leanprover-community/mathlib4), a single coherent library of
formalized mathematics past
[500,000 items](https://lean-lang.org/use-cases/mathlib/), built by hundreds of contributors,
with tactic automation accumulated over a decade. That library is the moat. It is why DeepMind's
AlphaProof formalized IMO problems in Lean (July 2024), why the
[Mathlib Initiative's 2025–26 roadmap](https://mathlib-initiative.org/roadmap/) includes monthly
dataset publication for AI training, and why "verify this algorithm" increasingly defaults to
Lean: the mathematics your proof needs is probably already there.

## What Bend2 claims

Bend2's dependent types come from the same intellectual tradition by a different road. Higher
Order Company's earlier proof language, [Kind](https://github.com/HigherOrderCO/Kind), is the
visible ancestor, and Taelin's public statements through mid-2026 describe Bend2 as combining
that type system with the [HVM4](https://github.com/HigherOrderCO/HVM4) interaction-net runtime
and a synthesis component, SupGen, named on his
[2026-03-05 launch-blocker list](https://x.com/VictorTaelin/status/2029567059881857081). The
declared shape: types precise enough to specify behavior, a checker that rejects wrong
implementations, a generator that searches for right ones, and evaluation that parallelizes
without annotation. The language was
[declared done on 2026-07-18](https://x.com/VictorTaelin/status/2078553927268589989) and remains
unreleased as of 2026-08-05, expected around [2026-08-12](/notes/bend2-release-date/).

Bend2's type theory got its sharpest public description on 2026-08-05, in replies translated
from Portuguese, posted while Taelin was mid-review of the core. Linearity with no hidden
exceptions: a plain binder is at most one live use, for any type, duplication is written `+x`,
and the license to duplicate is reserved for types of kind `Data`. A checker split into a Dead
mode, where types and specifications live unrestricted and may diverge, and a Live mode, where
code and proofs are linear and terminating, with the boundary sealed. The seal is the claimed
answer to the question a Lean reader asks first: Bend2 uses `Type : Type`, which Girard's
paradox makes inconsistent as a logic, and the mode separation is supposed to keep
paradox-shaped terms on the Dead side, where nothing is being proved. Lean buys the same
guarantee with a universe hierarchy and a termination checker. Whether the seal holds waits
for the checker's source, and the same replies say that source, `bend.ts`, is still being
aligned with this model.

## Same types, different jobs

Bend2 and Lean both live on the propositions-as-types side of the Curry–Howard correspondence:
a specification is a type, a proof is a program, checking is type checking. What differs is
which side of the correspondence pays the bills. In Lean, the proof is the product. You
formalize because the theorem matters, or because the algorithm's correctness matters, and the
executable is often incidental. Automation means tactics: decision procedures, simp sets,
`omega`, a decade of glue that discharges the boring 80% of obligations. In Bend2's claimed
design, the program is the product. Types exist to make machine-generated code checkable, so
synthesis can propose and the checker can dispose. Automation means SupGen, and if the
[superposition primitives](/notes/hvm4-explained/) in HVM4 are its mechanism, generation is
evaluator-level search over candidate programs rather than tactic-level search over proof terms.
That is a real architectural difference, and it is also entirely unverified until code lands.

## Execution

Bend2's runtime story has no counterpart in Lean, and vice versa. Lean compiles to efficient
sequential C; concurrency is orchestrated with tasks, not extracted from program semantics, and
nobody chooses Lean because their proof needs a GPU. Bend2's entire premise is that evaluation
itself is parallel: interaction-net reduction spreads across cores and, per the
[2026-07-18 CUDA report](https://x.com/VictorTaelin/status/2078471338755232193), across RTX
hardware faster than its Metal reference. If your verified algorithm needs to run at scale,
Lean's answer is to extract or reimplement in something fast and trust the correspondence;
Bend2's claim is that the verified artifact is already the fast artifact.

## Side by side

Bend2 next to Lean 4, as of 2026-08-04; the library row is the whole story.

| | Lean 4 | Bend2 |
| --- | --- | --- |
| Center of mass | Formalized mathematics, verification | Parallel execution, synthesis (claimed) |
| Status 2026-08-04 | Mature, FRO-stewarded, self-hosted | Unreleased, expected ≈ 2026-08-12 |
| Library | mathlib, 500k+ items, hundreds of contributors | None public |
| Automation | Tactics, decision procedures | SupGen synthesis (claimed) |
| Runtime | Compiled via C, refcounted, sequential + tasks | HVM4 interaction nets, parallel by default |
| License | Apache 2 | None published |
| Hiring/community | Large, academic and industrial | Does not exist yet |

## Which to use

Between Bend2 and Lean, Lean is the correct default today for anything that needs a proof:
verified algorithms, formalized specs, mathematics, AI-assisted theorem proving. The library
asymmetry is not close, and it compounds, because every mathlib contribution makes the next
proof cheaper. The
question Bend2 poses is narrower and sharper: whether proofs can be a byproduct of ordinary
engineering, attached to code that runs fast in parallel, generated more than written. Lean
was not built to answer that; Kind tried and stayed niche; Bend2 is the funded, about-to-ship
attempt. Both can be true at once, because nothing Bend2 ships subtracts from mathlib. This
page will be rewritten against the released compiler when code lands.