Bend2 vs Lean

Last updated 2026-08-05.

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 developed under Leonardo de Moura, stewarded since 2023 by the Lean FRO, Apache 2 licensed, with its own system description. 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, a single coherent library of formalized mathematics past 500,000 items, 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 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, is the visible ancestor, and Taelin’s public statements through mid-2026 describe Bend2 as combining that type system with the HVM4 interaction-net runtime and a synthesis component, SupGen, named on his 2026-03-05 launch-blocker list. 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 and remains unreleased as of 2026-08-05, expected around 2026-08-12.

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 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, 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.

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.