From the article:

At the risk of simplifying matters to a ridiculous degree, we might say that “types are like disjoint sets”; each element in type theory “is an element of” exactly one type. The type of the natural number 2 is the natural number type; the type of e, the base of the natural logarithm, is the real number type, and so forth. The type of natural numbers is disjoint from the type of real numbers, and an explicit coercion (sending 2 to 2.0) is constructed from the type of natural numbers to the type of real numbers. When I give talks, I sometimes draw a picture of sets as a Venn diagram with nonempty intersections and a picture of types as bricks stacked against one another without intersection.

[...]

The “summer of Lean soundness bugs” might sound like a disaster, but closer investigation shows that the detection of these soundness bugs is a positive development. The summer bugs were detected by frontier model AI in the hands of security researchers interested in reliable kernels, not by black-hat hackers. The Collatz bug was found by Ramana Kumar, a co-author of “CakeML: a verified implementation of ML”, which creates an end-to-end verified ML (the functional programming language). Several bugs were found by Dan Selsam. According to de Moura’s report, “Daniel Selsam at OpenAI assisted the Lean FRO with an AI specialized in cybersecurity, and found other programming mistakes in the Lean kernel. All of them have been fixed.” The collaboration with Selsam ended “when the internal AI reported it could not find additional issues.” Dan Selsam has contributed to Lean from its early days and was one of the creators of the IMO grand challenge aimed at achieving IMO-level problem solving verified in Lean. He has been in the news recently over his warning about AI safety (Sept 14), reported in a viral post on X.com.

[...]

In a post online on September 10, Joachim Breitner wrote, “I’m a bit childishly proud that I just released a Lean Checker with a formal consistency proof. I declare the summer of AI-found kernel implementation bugs to be over!” (@nomeata). I would go further and describe this project as one of the most important milestones in Lean’s history.

Breitner has developed a verified Lean kernel called Con-Leche. The implementation is in Lean, and consistency is formalized in Lean, with code and proofs generated by Claude. The formal consistency proof assumes a Lean encoding of ZF set theory augmented by a hierarchy of inaccessible cardinals. Interestingly, the Con-Leche semantics for Lean’s terms are directly set-theoretic rather than type theoretic. Con-Leche has checked mathlib. The project contains the usual disclaimers that the kernel verification makes assumptions about compiler, runtime, and computer environment. Con-Leche’s consistency proof has been checked by more than a dozen other proof-checkers. Con-Leche’s consistency claim might suffice for all practical purposes, even if it differs in technical detail from the claim of Lean type-theory consistency.

One highly positive aspect of Breitner’s work is that some of the most abstruse parts of Lean, such as the general machinery of mutually inductive types with nesting, now have consistency guarantees backed by a set-theoretic model.

[...]

Above in our “ridiculous” simplification of type theory, we stated that each term has a unique type. More precisely, unique typing is the property that if a term has both type A and type B, then A and B are definitionally equal. Unique typing is not a property built into Lean’s logic. It is a tricky conjecture that is still unproved. Other very basic questions about Lean’s type theory remain unanswered, including Pi-injectivity, a modified Church-Rosser property, and sort injectivity.

[...]

This property states that there is no derivation of False in Lean’s system with the given axioms, under the assumption of set theory consistency (with suitable axioms). Of course, logical consistency is the single most important property that we should desire of Lean’s type theory. As of October, 2026, I know of no complete, public relative-consistency proof covering Lean abstract type theory. Mario Carneiro has claimed in his thesis and in lectures that there is an alternate route to establish consistency that avoids the thesis error, but to the best of my knowledge, this alternate route has never been written down, beyond a brief statement in the introduction to his thesis. In my view, a result of such fundamental importance must be given in full before it is accepted. Con-Leche, discussed above, makes and formally verifies a closely related consistency claim relative to set theory.