Lean now ships with verified kernels | Hacker News Reader

Lean now ships with verified kernels

leodemoura.github.io

204 pointsmatt_d81 comments

Suppose lean in its current state existed 15 years ago, and suppose the math community eagerly started contributing en masse to a shared repository of code. How much of the breakthroughs and longstanding questions in mathematics that we’ve seen answered this year do you think we would have solved?

In other words, how much of the developments this year are directly attributable to LLMs using lean, versus lean just being a significantly more productive language for some subset of mathematics compared to English and LaTeX?

Given how much we’ve seen formalized this year it feels hard to believe that this couldn’t have happened earlier.

Follow up question: do you think mathematicians would be as upset about the rapid changes in their field if they were the result of a collective shared effort on github, authored entirely by humans who all share the credit, versus that same outcome but authored by a large language model?

In other words, are the mathematicians upset about large language models, or are they really just upset that formalization and massive collaboration have turned out to be highly effective and has negated the heroic angle that mathematicians previously enjoyed, thinking in a locked room by themselves?

Food for thought.

A coworker recently remarked that lean seems like a new foundational language family that every programmer should be able to read, on par with C and Python, and I think it’s pretty hard to disagree with that. Next generations of models are going to be RL’d on Lean more and more because it pays dividends in winning the math war against their competitors, and this will benefit users of lean not only for mathematics but also as a general programming language and as a vehicle for other DSLs. For example, I think Sparkle (a Lean based HDL) or something like it makes a lot of sense in 2026 and beyond.

https://github.com/Verilean/sparkle

> Suppose lean in its current state existed 15 years ago, and suppose the math community eagerly started contributing en masse to a shared repository of code. How much of the breakthroughs and longstanding questions in mathematics that we’ve seen answered this year do you think we would have solved?

(Former grad student in math here who has spent whole weeks formalizing in Lean lemmas that would be considered by professional mathematicians writing a mathematics text / paper as obvious ("without loss of generality we can assume that....", "it should be clear that...")

Probably very few or none.

These systems (mostly) don't help you discover new mathematics. They are a tool for formalization.

It just turns out that combining them with LLMs is the secret sauce. LLMs have quite a bit of creativity but make a lot of mistakes. The Lean typechecker never makes a mistake but has no creativity. Get them to work together in an iterative loop and you get what we have now.

I am a math undergrad and I tried lean. It probably is because of habit and familiarity but I still find lean proofs harder to read than NL proofs. I wonder what if the math education switch entirely to a formal language (not necessarily Lean) will be?

"Mathematics is commonly explained and recorded in symbolic and concrete forms that are easy to communicate, rather than in conceptual forms that are easy to understand once communicated. Translation in the direction conceptual -> concrete and symbolic is much easier than translation in the reverse direction, and symbolic forms often replaces the conceptual forms of understanding."

https://mathoverflow.net/questions/43690/whats-a-mathematici...

Ask a model (dsv4.1 flash works great on this) to explain the proof to you so you can get an idea of the overall concept and structure first. Formalized math tends to encode math a certain way to make it easier for Lean, which doesn't have a visual cortex, but harder for people.

As a former math major (and developer) it bugged me that lean is optimized for WRITING proofs and not for READING proofs. I'm noodling around with a language that is optimized for reading proofs:

https://github.com/ityonemo/2b4m

The tradeoff is that it's more verbose, but you don't have to even know the language to properly decode a proof.

as an exercise for the language, I'm playing around with having Claude formalize an online algebra text:

https://github.com/ityonemo/2b4m/tree/main/aata

LMK what you think

Putting aside the Claudisms.

You only compare to tactic heavy languages, which is what you don't like about them. Try looking at Agda, Idris, Mikan,... They work with pattern matching not just for definitions but for proofs as well, so the derivation is laid bear.

Not saying your niche doesn't have value, but you can get interesting ideas from there.

Thanks, good advice!

Aside: To some degree, the claudisms are the point since the PL is written by Claude and intended to be consumed by claude

Re aside: Ok, but consider that maybe it is rude to ask people to read something you didn't write without warning. I'd add a disclaimer whenever I post about it, and on the very top of the readme. Better: have a readme for humans that you wrote, and leave the current document as a readme for machines.

i feel like this would be the equivalent of having all CS undergrads program with assembly and assembly only.

it might(?) work? but abstractions exist for a reason (mostly...)

It's completely different things. Math itself is abstraction. Lean is formalized abstraction that don't let you write "it is immediately obvious that"

Lean tactics can handle obvious things automatically, for some value of "obvious".

I think this is kinda the problem with lean, to be frank. Sometimes it's not obvious what lean is doing. (unless you're interactive)

Knowing very little about lean but speculating here: is lean something that could output a few natural language expressions at key points so that you can still have “it should be clear that” for the natural language reader but have it undeniably proven.

Ie entrust the more tedious aspects but be able to follow along and still have references to check if you are curious about thoroughness.

Almost like a tap with a latex renderer at various insertion points?

I have hear people make this comparison many times, but it just does not hold up under scrutiny.

I think the confusion stems from people being exposed to set theory, believing that formalisation is akin to writing those horrible set encodings of everything. Which I would agree would be akin to writing assembly.

But Lean, Rocq and Agda are all based in type theory. Which means it is more like the highest level programming language you can imagine! You have all the powers of abstraction, but you still have to convince the type checker – i.e. no “trust me, bro” casting, or even questionable while loops (“I promise this loop finishes at some point”).

These abstractions along with meta programming techniques (“tactics”) means that you can write readable correct proofs, but it takes effort. Math is extremely deep, and getting formalised all the way to the research frontier in a given subfield is a serious undertaking.

I think a lot of people have never actually tried using a proof checker and are forming hot takes based on their imagined assumptions about how they work.

For anyone reading this, here is a very small example proof that + is associative over Nats in Agda (written using 1lab style equational reasoning syntax):

    +-associative : (x y z : Nat) → x + (y + z) ≡ (x + y) + z
    +-associative zero y z = refl
    +-associative (suc x) y z =
      suc x + (y + z) ≡⟨ ap suc (+-associative x y z) ⟩
      suc (x + y + z) ≡⟨⟩
      (suc x + y) + z ∎

We pattern match on the first nat to get `zero` and `suc x`. In the `zero` case we have `0 + (y + z) = (0 + y) + z`. Both sides compute to `y + z` and thus the equation holds by reflexivity.

In the `suc x` case we need to show that `suc x + (y + z) ≡ (suc x + y) + z`.

`suc x + (y + z)` computes to `suc (x + (y + z))` by the definition of `+`.

By recursively calling `+-associative x y z` we get `x + (y + z) ≡ (x + y) + z`. Then we need to prove that by congruence this is true under `suc`. We get this by passing our proof (from the recursive call to +-associative) into `ap suc`. `ap` says that given `a = b` it is true that `f a = f b`.

Finally, `(suc x + y) + z` computes to `suc ((x + y) + z)`, so the last step holds by computation, which is why it’s just `≡⟨⟩`.

Proof checkers like Lean/Agda/Rocq are literally total functional programming languages with rich type systems.

Everything above comes down to pattern matching and function application. The proof is just a function whose type is the statement we wanted to prove, and the type checker accepting it is what makes it a proof.

This is the Curry-Howard Correspondence in a nutshell. Propositions are types and proofs are programs.

And here is another short and simple example of some Agda code (Did you know you can open modules in a type signature‽):

    -- An element has at most one two-sided inverse.
    inverse-unique : ∀ (M : Monoid) (open Reasoning M)
                       (x y z : type M)
                   → y ⋆ x ＝ unit M
                   → x ⋆ z ＝ unit M
                   → y ＝ z
    inverse-unique M x y z leftInverse rightInverse =
      begin
        y                ⟪ sym (unitᵣAt y)           ⟫
        y ⋆ unit M       ⟪ mapᵣ (sym rightInverse)   ⟫
        y ⋆ (x ⋆ z)      ⟪ sym (associativeAt y x z) ⟫
        (y ⋆ x) ⋆ z      ⟪ mapₗ leftInverse          ⟫
        unit M ⋆ z       ⟪ unitₗAt z                 ⟫
        z
      ∎
      where open Reasoning M

Not sure if all the unicode characters will render on HN, but the things left of the ⟪ ⟫-brackets is exactly what a text book in mathematics will have. While the things inside the brackets are just a functional-programming way of saying out the argument which would be left for the reader to make in their head for why each step holds.

(If you know Agda, I dare you to look carefully at this example!)

Once upon a time this was all there was, so it naturally was proven to work as it was easier than dealing with boards full of dip switches that predated them.

Naturally eventually we got macro Assemblers, followed by other attempts until FORTRAN came to be.

Assembly doesn't give you any safety or guardrails. It is basically the opposite. I think it would be a better comparison with something that is a very strictly typed and type checked language.

Is that because you were starting from scratch and working alone, though?

Imagine a hypothetical project at the scale of the Linux kernel, with thousands of mathematicians building up organized and well-commented code, standing on each others shoulders.

(not a mathematician, but I played with lean as a hobby). No, this already existed - lean standard library was basically this, with hundreds of mathematicians working together to formalize basics of currently known math. But this is just very slow for a human.

I remember there being whole research groups trying to formalize a single (real world, as opposed to undergraduate) proof, and I remember reading that formalizing something like FLT is currently completely unfeasible.

In short, no, lean was not a tool to discover new math.

> formalizing something like FLT is currently completely unfeasible.

No, Kevin Buzzard is leading a project to formalise FLT for a couple of years now. Anthropic scooped him last month, but his project involves more than just producing a formal proof: https://xenaproject.wordpress.com/2026/09/04/flt-anthropic-h...

Anthropic formalized FLT in 11 days: https://www.anthropic.com/research/formalizing-fermats-last-...

Make a trivial adjustment to your final proposition and it would still hold, no?

> Humans have quite a bit of creativity but make a lot of mistakes. The Lean typecheck never makes a mistake but has no creativity. Get them to work together in an iterative loop and you get what we have now.

It's less useful, because humans make fewer mistakes and take longer to turn their thoughts into Lean. I think most mathematicians have a higher success rate thinking about the problem informally, poking at it themselves, then formalizing it iteratively to make it more watertight as they gain confidence in the idea.

> humans make fewer mistakes

Is this empirically measurable?

The speed matters massively. Also it seems that LLMs are... getting to be quite creative.

The point is that the there has to be an idea to try to check. Lean does not give you that.

But a human being using LLMs will be much more creative than just LLMs alone right? Or does the human reduce the creativity in this system in your opinion?

> But a human being using LLMs will be much more creative than just LLMs alone right?

I believe so. But the question I was responding to was whether humans working with Lean would be have been more creative.

> Or does the human reduce the creativity in this system in your opinion?

Yes. Humans are slow.

Absolutely none of them. I have some experience formalizing math by hand in the pre-LLM era. I never started with making the formal proof. It is way too difficult. I don't think I've ever heard of any mathematician starting with a formal proof vs writing a natural language proof. Starting with a formal proof vs a natural language proof is putting the cart before the horse.

Without a natural language proof, or at least an idea of how to write the natural language proof, it is very difficult to write a formal proof. It's flying blind. I can blindly apply tactics, but without some larger plan to guide my formal proof, it's near impossible to make progress on all but the most trivial proofs. I don't think it has ever happened that a major proof was formalized before its natural language proof was written.

I don't think people appreciate just how labor-intensive it previously was to write a formal proof. It takes easily 10-1000x as much time for a human to write a formal proof vs a natural language proof. Even just formalizing a single undergraduate math textbook for certain subjects by hand was considered a multi-year project for a professional mathematician to undertake.

Formalizing a new paper, even if it was building on previously already formalized theorems, could be months of work just by itself, even with the natural language proof in hand.

It is no surprise that OpenAI releases natural language proofs before they release formal proofs. Presumably the same difficulty difference applies to LLMs as well.

OpenAI having NL proofs earlier than Lean ones would require trust in the proof without ability to check it automatically. Perhaps Lean proofs are published later because it is considered a less important implementation detail or because there is a cleanup step that takes time.

No it's already explicitly stated that translation to lean is a second step that happens after NL proof is done. That's why some of 400 paper dump is without lean proofs.

I wonder how are they sure the proof is correct before making a Lean translation. How is the work loop organised to force LLMs to reach a valid solution. I thought the ability to make it possible was the main advantage of using Lean.

This is my hypothesis too. I work with LLMs daily. I use frontier models all the time, and I work in a startup that trains its own special-purpose models. At no point in the course of my work do I see anything resembling superhuman intelligence. I see superhuman stupidity, ie. stupidity so extreme that it exceeds what any human is capable of by orders of magnitude. So where are the superhuman math results coming from? Simple: translation. I've already thought this for a long time, that math is an obsfucated field and that programming already makes it far simpler to understand. So you train a machine to throw tons of compute at translating math into programming, and blow the field out of the water because it's effectively been deobfuscated. Math proofs had a sort of security by obscurity; they were not genuinely supremely difficult, but rather very few people worldwide worked on them and their work was heavily obscured, so the great deobfuscation machine comes along and trivialises that aspect and suddenly the facade crumbles. I think all of this could have been achieved a long time ago had humans done the deobfuscation, but there wasn't sufficient programming <--> maths cross-domain expertise or financial incentive to develop it.

This is not at all what mathematitians are saying. They say LLMs obfuscate proofs even more. Saying that mathematitians obscure proofs is nonsense. Maths requieres a big effort from the brain to be deobfuscated as you say, and deobfuscating maths requires understanding, which takes even longer. Thats why textbooks dont exist just after a new proof appears, it takes some time to digest it and identify the key parts.

Maths is a language, and learning a language takes time. Its like if I say that japanese made an effort to obfuscate their language just because i cannot read it or read it as fast as english.

LLMs are autimating some part of maths which is formal manipulation. It happens that computers are much better than humans at formal manipulation. In the same way that computers are much better at mathematical computations. That is the huge change in the field. But any working mathematitian can tell you that formal manipulation is just part of the research job.

The powerfull thing about maths is that formal manipulation has allowed humans to go further "for free": you just need to understand the foundations, and the formal system allows you to compute new results for free without needing to reunderstand them.

I am really curious how far you went in math, because you seem incredibly ill-informed.

It is certainly a 'unique' perspective.

Reading very charitably: you can say that at the moment a lot of the AI's advantages seem to come from: (a) having read approximately everything, and (b) being willing and able to try out lots and lots of approaches without tiring or getting bored. You don't need to have superhuman intelligence, yet, when superhuman persistence still yields so much low hanging fruit.

It's not unique. I for one agree. Mathematics is obfuscated because mathematicians prioritize compactness on the page over ease of understanding. This results in confusing notation (single-character variable names, implicit multiplication, implicit parentheses) and large numbers of omitted steps.

If I want to understand some mathematics, my first step is always translating it to code. Modern code (excluding array languages) no longer has a culture of minimizing character count, and omitting "obvious" steps is not possible. LLMs are based on an architecture (transformers) that was originally designed for natural language translation, so it doesn't surprise me that they're good at this.

The concise notation and omitted steps are to increase legibility. You are focused on things that the author is intentionally telling you are not important, and you are likely missing the things they're trying to say (e.g. the "shape" of an expression vs the names/super concrete meanings of variables). One of the challenges with Lean is that it requires a lot more effort to write things in a way that communicates what you're actually trying to say.

You need to think of mathematical writing as being both symbols/words and also a picture. You're meant to see patterns in what is in front of you. The short names are necessary for the picture. Without them you can't see it. It's like you've zoomed into the individual pixels; the information is all there but you'll never make sense of it that way. You're meant to read the "zoomed out" view where you have short placeholders as names.

And anyone who's tried to write or read Lean will also tell you that understanding a complicated mathematical proof doesn't necessarily get any easier when it's completely formalised.

Had the same problem with browser extension for a while. I made Explayn because of it: a browser extension that explains any highlighted word, sentence, or formula in place, so readers can understand content without leaving the page. https://chromewebstore.google.com/detail/enjakhegoldmloghmce... Figured it might save you some time.

yes, I couldn't agree more, if like to add that "the industry" drove programming and maths apart:

computer science, or "Informatik/informatique" how some Europeans call it, was a branch of mathematics, and "the industry" pushed _very_ hard to get it "practical", make colleges and universities produce programmers, not computer scientists.

so they removed all "challenging" maths requirements from the curriculum, and you can graduate with much less formal rigour, and certainly without being a matematician.

that's also how python replaced scheme as a first teaching language.

> that's also how python replaced scheme as a first teaching language.

Not so fast. There were plenty more horses in that race.

You can easily make an argument that Python is a 'worse' language than Scheme as a first teaching language (though not necessarily one I would subscribe to: they are both dynamically typed and mostly differ in syntax). But Python (and Scheme and even Basic) are a lot better than starting people off with C or Java, or, God forbid, C++.

Obviously there are people who you can lock in a dimly lit closet with just an outdated reference manual to a made up machine and they'll can't help but pick up programming; and those won't have much trouble coping with Java or C++. But those who actually need to be taught will be better off with Python (and Scheme).

This is a good thing, it was just implemented the wrong way. Should have split the degree into separate engineering and theoretical tracks with different names (CS and CE/SE). Today we get weird hybrids where the same degree is math focused in one school and more practical in another.

There is space for both but in the real world we need more engineers who know how to build systems properly than theorists who are great at formal reasoning. It's like structural engineering and physics.

While I think there is some truth to this I think the framing is very uncharitable. The obscurity in maths comes from layers upon layers of abstraction because this is a useful way for humans to work with these complex ideas. I think we see some of this with these proofs that have been translated to lean: some of the proofs are millions of lines of lean, imagine trying to wrap your head around a codebase that is millions of lines! And just for a single proof! These impenetrable abstractions that mathematicians have created are like a mental model for a massive code base.

I concur with one of the other replies: very few or none.

This is putting the cart before the horse: Progress in verification has been huge because of LLMs. Mathlib PRs spiked at the release of Opus 4.6, any of the big formalizations would not have been here without LLMs.

More surprising to me, OpenAI claims they're doing informal reasoning and only after do the formalization. This seems to match the way in which they release things. Of course they will have Lean in the training data, but I think this supports the mirror hypothesis: We'd have the same progress in mathematics if proof assistants didn't exist, it would just be a pain to verify correctness.

Fully agree on the potential for Lean as a generic programming language.

Hell no. Writing formal proofs has huge overhead. Lean is not a productivity tool; it's a reliability tool. It's like asking if airport security made boarding faster.

Mathematicians are also not upset about Lean. They're upset because they feel like they're becoming redundant. And that has everything to do with LLMs and not Lean.

They're upset because they're having to change. They aren't being made redundant, but they're being made redundant for the part of math they most enjoy and for which they've traditionally been most rewarded.

I don't understand what you're saying. Writing lean doesn't make it easier to formulate a proof. These LLMs are writing natural language proofs then formalizing after the NL proof is done. If humans were theorizing and exploring open problems in lean for the last 15 years, we'd be moving much slower than we have been with natural language.

Funnily NL is indeed different from formal language and does different in a way that makes a difference: https://www.scientificamerican.com/article/openais-blockbust...

This is a great question. I am not a mathematician but I've had similar questions about my own field (CS/Elec) as well.

I have always felt that a huge amount of brain power has to be expended in understanding the jargon and getting used to the machinery. Once we get past that, what people would think are highly challenging subjects become rather simple and logical. An analogy I like to use is old people struggling with simple tech tasks. I remember an uncle of mine who approached me to fix their laptop which wasn't connecting to the internet. Turns out the laptop had not been booted in a while and the public certs shipped with the machine had expired. Said person is a highly accomplished person in their field but was helpless when it came to this task. After I solved the issue, the uncle was eager to know what the problem was and I tried to ELI5 it but to no avail. It is possible I did a really bad job of explaining it but there was too much basic machinery to cover. Why is there a public and private key, what is symmetric/asymmetric, why do certs even expire etc. I couldn't even touch on the foundational math underpinning all of it so I left him in a confused daze.

To any SWE, all this is table stakes but for non-tech people it is way too much jargon. Today, I'm confident my uncle could prompt his way to a working understanding of PKI - heck maybe even some aspects of cryptography and prime number math that makes it work. This is where I see LLMs making a massive difference - they can crunch a massive amount of jargon and leave only the actual trick/idea for you to understand.

This is also what people like Szegedy and Tao have also said - LLMs will make math closer to what SWE is - a lot more people doing it in workmanlike fashion rather than a small community writing papers. At one point, dynamic programming was some research topic that Bellman worked on and now every 20 year old works on tens to hundreds of these problems in the hopes of cracking a job. But I'm sure the Math field will go through some turbulence and I wish them the best. There will always be a need for SMEs who deeply understand a subject and can come up with interesting problems.

> A coworker recently remarked that lean seems like a new foundational language family that every programmer should be able to read, on par with C and Python, and I think it’s pretty hard to disagree with that.

Lean isn't super special in that regard. If you know Haskell or OCaml you are already pretty far along in at least being able to read Lean, as it comes out of a similar-enough tradition.

I would argue that it's pretty damn far from the Agda/Coq/lean world.

You really have to wrap your head around dependent types and _≡_. In my experience it was far more mind blowing than just FP.

GADTs and a few of the wilder Haskell extensions sort-of go a bit in that direction.

But yes, you have to wrap your head around dependent types.

> If you know Haskell or OCaml you are already pretty far along in at least being able to read Lean

But that's not really what you want, right? Speaking as a programmer, I'd think you would want a language where the prerequisite is "knowing a math proof", not "some mathey PL"

> every programmer should be able to read

You want "every math major should be able to read it", not "every programmer"

> But that's not really what you want, right? Speaking as a programmer, I'd think you would want a language where the prerequisite is "knowing a math proof", not "some mathey PL"

Well, I was merely replying to this:

> [...] lean seems like a new foundational language family that every programmer should be able to read, [...]

The OpenAI proofs were all in English, and discovered by reasoning in English. Only afterwards was a portion of them translated into Lean. This step was only done to convince the mathematicians that the proofs were correct.

I think you have it backwards-- formalization is tedious and seldom yields insight.

It's the kind of low yield completionist task that you just don't do without something equivalent to cheap slave labor.

AI makes formalization more accessible and makes it more important: The current superpower of LLM powered research is that the LLM is absolutely relentless, but the relentless is a liability without a source of truth to check against.

I remember attending a talk about Lean well before LLMs or the current AI craze. They were trying to automate mathematics for a long time.

While everything seems crazy right now, the building blocks have been coming together for a long time now.

> A coworker recently remarked that lean seems like a new foundational language family that every programmer should be able to read

Extraordinary claim requires extraordinary evidence.

Why? I’ve worked a bit with proving systems in my studies, but it seems to me that it is very hard to turn precise mathematical statements into useful programs. Perhaps for the core logic, but GUIs or any other state with the outside world is going to be difficult it seems to me

I mean we had Coq for the longest time.

Yeah, it's so funny seeing all these people discover Lean as if it invented mechanizing mathematics. Even Coq wasn't the first (might have been the first with dependent types though).

Now that the clankers do the work, programmers are suddenly interested in Lean, which has been available since around 2014.

Software "engineers" really just want to be button pushers and design overly complex Rube Goldberg machines.

Waiting for "i made this" posts for formalized code ...

Sorry for almost completely unrelated shower thought but: there is an opportunity to name your blog “Leanardo”

What does “verified” mean here? Someone has formalized verified the kernels or just different kernels cross check each others?

They created an implementation of a Lean kernel in Lean (con-leche) and verified it as consistent.

Since there can be bugs in its compiler and runtime, they translated the code into Rust (con-ron), and verified the resulting kernel with another Rust-based verification tool.

There is also an ongoing verification project of Lean4, which is written in Lean4 itself. (My mental model is Lean4 := Raku and Lean := Perl)

So we have two verified kernels now, and another is awaiting release.

But is this cyclic? also no matter what we do we will hit Godel?

For the highlighted kernel (con-leche) , they postulate a set theory. Godel doesn't get involved because the proof is effectively saying Lean+ZFC entails Con(Lean), but even that isn't quite right, because the kernel doesn't include all the features of Lean. But even that isn't quite right, because they're actively modifying the kernel to be "simpler" to check.

It's a marketing post at the end of the day is what I'm trying to say. Regardless, Lean is probably the most trustworthy proof assistant on the planet at this point.

What’s more interesting to me is the fact that these two kernels (con-leche and con-ron) were actually implemented by Claude (with “human supervision”).

Programming as a hand-crafted art is really diminishing fast.

Rocq (Coq) and Isabelle/HOL?

Rocq has had similar issues with AI finding soundness bugs, particularly in module code last I checked. Yet they don't even have half the resources of Lean. Rocq is nowhere close in my opinion. Though this is really like comparing how many 9s. If Lean is 99.9999% trustworthy, than Rocq is 99.99% trustworthy.

Isabelle/HOL is probably at similar footing to Lean because its kernel is so simple.

The question is if Godel matters in practice, or if its is just a limiting behaviour with infinite resources

> we will hit Godel

It seems no one understands how useless this theorem is in practice.

both

As someone who doesn't quite get all this, isn't the proposal here just checkers all the way down?

The proposal is that multiple checkers are unlikely to all have the same bugs so the more kernels you can use to check the results the more likely it is that the proof/code is consistent & correct (modulo set theoretic assumptions necessary for the correctness of the kernel).

Lean plus AI is a winning combo: Lean is super precise but "narrow", AI is broad but lacks precision.

Before AI it was super tedious to formally express your software models in Lean, with AI this is super easy. See formal verification of consensus core in Ultima Cluster: https://github.com/PeterKnego/ultima_cluster/blob/main/docs/...

> any remaining unsoundness bugs are most likely in Lean's compiler or runtime (including the bignum library). It is very unlikely that the same bug also exists in the Rust compiler or runtime, so by checking a proof with both con-leche and con-ron, you gain a high level of protection against this class of bugs

An awful lot of references for arbitrary precision arithmetic are just repackaging Knuth’s explanations, so I wonder if there could in fact be a bug in common (Although you would like to assume every other piece of software using them would have also hit any issues by now, so maybe it is fine)

Why not verify a Lean kernel with something other than Lean?

“ AI agents are very effective at finding vulnerabilities in our software.” No! AI can find code weaknesses not vulnerabilities. All vulnerabilities are weaknesses, but not all weaknesses are vulnerabilities.

Reply on news.ycombinator.com