Rendered at 22:17:26 GMT+0000 (Coordinated Universal Time) with Cloudflare Workers.
chr15m 21 hours ago [-]
Will we ever see a soundness bug in the lean kernel again?
To a software developer the question seems insane. There were bugs in the past, of course there will be more.
When we see those bugs, what will it mean for AI lean proofs? Can we trust them?
This whole thing boils down to trust.
We can trust human verifications highly because of community and reputation and human proof-of-work. Humans sometimes lie about math results but it's rare because of this. They make mistakes and those mistakes are discovered by communities who are themselves largely trustworthy because of this.
LLMs don't care about reputation. They hallucinate and fabricate often. In harnesses they literally try to cheat and bend rules, which is a disaster for knowledge that is encoded in rules. So we have to rely on proof checkers.
The problem is, how trustworthy are proof checkers? Are there bugs? And is the underlying theory itself free of paradoxes and unknowables and mathematical "bugs" that can be exploited? Imagine a human mathematician hell bent on deceiving other mathematicians - would we trust their breakthroughs, even with a verifier?
Because of these properties, the final backstop has to be humans, and rooted in the community and proof-of-work based human trust system. At the moment people are trusting the tools too much.
Prediction: bugs will be found by humans using AI tools that call into question the Navier-Stokes proof.
plesiv 18 hours ago [-]
The existence of an undiscovered soundness bug doesn't make everything proven in Lean illicit. The proof would have to exploit the bug. People build houses on sound foundations even though the tectonic situation under them might not be sound.
> Because of these properties, the final backstop has to be humans...
The post has clearly stated that the work on Lean's underlying metatheory is not done, and requires more work. It's not inconceivable that computer formal verification could reach the trustworthiness of math itself.
chr15m 17 hours ago [-]
> The existence of an undiscovered soundness bug doesn't make everything proven in Lean illicit. The proof would have to exploit the bug.
Yes, correct. The proofs would have to be checked to make sure they don't exploit the bug.
> computer formal verification could reach the trustworthiness of math itself.
Yes, it could. I don't think that is currently the case.
Alive-in-2025 5 hours ago [-]
It's just turtles all the way down. This is not different than the fact we know as programmers there are bugs in the tools and compilers we use, they get fixed over time but more bugs remain. It is frustrating to realize that we aren't on solid ground like we want to be.
Do you trust the result of your c++ program is correct? Because there are bugs in every compiler, language. You passed that million test correctness checker on the new version of the compiler, but it didn't catch everything.
When a bug is fixed, you don't immediately retry all existing results from your application program. Maybe you would if the bug was in some area you know was important and exercised by your code, say you were adding and multiplying numbers and bugs were found in that area.
The checker has a bug, the compiler the checker was testing had a bug, your own code that was compiled by the compiler had a bug probably. There can be bugs at any layer.
omnicognate 14 hours ago [-]
> not inconceivable that computer formal verification could reach the trustworthiness of math itself
Not entirely sure what you mean by this, but every interpretation I can think of is AFAIK (I am not a mathematician) indeed inconceivable by Gödel's incompleteness theorem. As the article says the only thing it's mathematically possible for us to get out of formal verification is a proof of consistency relative to (i.e. assuming the soundness of) some other system. As far as formal verification of "math itself" is concerned it's turtles all the way down.
Edit: Oh, do you mean that we could come to trust formal verification as much as we trust (well established) maths generally? That's a different speculation entirely and not an objective or well specicified one. There are plenty of people on this site who already trust a Lean proof more than a traditional one, without understanding either.
chrisjj 3 hours ago [-]
> People build houses on sound foundations even though the tectonic situation under them might not be sound.
Difference is, they don't then mistake the house as sound.
westurner 6 hours ago [-]
Noting that planes fly but there is yet no Lean proof of Bernoulli's principle in Mathlib or Physlib.
> the trustworthiness of math itself
Is abstract math rigorously proven?
dnautics 5 hours ago [-]
Isn't it the case that planes mostly fly because the wing has an angle of attack? (a fighter jet has no problem flying upside down)
dreamcompiler 4 hours ago [-]
Yes. The point of the airfoil shape is to make flying more efficient, i.e. the engine would need to generate much more power if the wings were flat slabs, but the plane could still fly given a big enough engine.*
*Assuming the "big engine" wasn't so heavy that it made flight impossible because of its weight.
westurner 5 hours ago [-]
It may be. Indeed how do helicopters even fly.
But the point is that Lean formalisation is a new bar for engineering and for physics and abstract math.
ziiinq 12 hours ago [-]
[dead]
cjfd 14 hours ago [-]
Sure, we are likely to see soundness bugs in the current lean kernel again. And in other proof assistants too. Regarding the correctness of proofs this is not the biggest worry, in my opinion, though. Both sides of attempting to get faulty proofs in and of strengthening the kernel to keep them out have AI on their side. If AI advances more and becomes smarter it can be used on both sides. And the defending side has the easier task here. I am not sure about the Navier-Stokes proof but in general it sounds highly unlikely that many well-known theorems turn out false.
The bigger worry are question that Terrence Tao is also talking about. I.e., is the proven theorem actually the theorem we are interested in? Are basic definitions of the field stated correctly? That kind of question. There is also still parts of proof assistants that are not the kernel and that can be abused. E.g., abuse the pretty printer/parser to make something look different from what it actually is. Introducing an axiom while typographically hiding that one was added. If I remember correctly I saw an example of the latter thing in the Coq (now Rocq) theorem prover many years ago. I forgot how it precisely went or where I read that.
chr15m 10 hours ago [-]
> If AI advances more and becomes smarter it can be used on both sides.
Yes, and that's true even if it doesn't advance or become smarter. It's happening already that people are using AI on "both sides" both adversarially and defensively and that is improving software, and hopefully mathematics as well.
> I am not sure about the Navier-Stokes proof but in general it sounds highly unlikely that many well-known theorems turn out false.
I'm talking about the LLM Navier-Stokes proof specifically because it's very long and complicated and an LLM is not the same as a human mathematician. A human mathematician is trying to use the tools in a truth-seeking way, whereas LLMs are trying to satisfy the goal of presenting a proof that convinces people it is correct. Maybe naively, it seems to me the failure modes of proof assistants would be amplified under adversarial conditions (i.e. driven by LLMs).
Completely agree that there seem to be many ways that relying on proof assistant software can go wrong.
Alive-in-2025 5 hours ago [-]
What happens when we have proofs that are too long for a human to understand, and only the llm can spend the perhaps years of human effort to verify things? That will happen.
With humans we break things down (proofs, new concepts) into digestible hunks for each other, because you want other people to understand them but also verify them. And it's less common for someone to build a tower of new intellectual things with 1,000 new connected ideas that prove things and build up together, that ends with P = NP after all or something.
So since we have these new tools that can chain things together more than we can, eventually there will be huge "proofs" where there are long chains of new ideas, concepts used to build up ever more in giant intellectual towers. And we can't verify/understand them, at least not for many many years.
I shudder to think of such a situation. We already have very important ideas that have no proofs, that people build on. Now build 100s of these things together.
jhanschoo 19 hours ago [-]
> The problem is, how trustworthy are proof checkers? Are there bugs? And is the underlying theory itself free of paradoxes and unknowables and mathematical "bugs" that can be exploited? Imagine a human mathematician hell bent on deceiving other mathematicians - would we trust their breakthroughs, even with a verifier?
---
> Autumn of verified Lean kernels
Have you read this section (and immediately following sections) in the article? It seems that it partly addresses your thoughts. Perhaps you should comment replying to it.
chr15m 16 hours ago [-]
> Autumn of verified Lean kernels
Above my pay grade, but it sounds like some kind of super cool self-hosted recursive lean-checker-in-lean.
I notice there are a bunch of caveats in that part of the article. If you were an LLM strongly RL'ed to give humans the result they're asking for, using recursion bugs to satisfy the goal would probably be something you would try.
I'm by no means an expert but I do think the old adage "great claims require great evidence" still applies, and a healthy dose of scepticism and epistemic humility is warranted.
jhanschoo 14 hours ago [-]
What do you mean by a "recursion bug"? The terminology does not occur in the article so it seems to be a term that means something to you that is not very clear to me.
chr15m 10 hours ago [-]
I am conflating (probably ignorantly) the idea in software development of bugs in recursive code, with the potential for bugs when using Lean to check Lean’s checker.
rramadass 11 hours ago [-]
> I do think the old adage "great claims require great evidence" still applies, and a healthy dose of scepticism and epistemic humility is warranted.
You are just making glib statements without having the necessary background. Hence it is difficult for people to engage with you since we have no idea whether what we say is understandable by you. I suggest that you go through some of the resources mentioned here (and other similar HN threads) to get some necessary background after which we all can have a better informative discussion.
How do you think Mathematicians were accepting each other's proofs before computers came along? They used a process like;
1) Relying on the prover's honesty (i.e. he is not intentionally trying to deceive).
2) Providing a mandatory proof idea (i.e. the main outline) for clear communication and comprehension.
3) Clear definitions/assumptions/statements of the problem/theorem to be proved.
4) Rigorous application of a few small logical reasoning steps viz. Deductive/Inductive reasoning, Logical Operations (specifically Implication/Converse/Inverse/Contrapositive), Rules of Inference, Quantifiers and basic structural conversions.
5) Walking through and validating the given proof by multiple mathematicians and ensuring that the results match. The Lean kernel can be considered as another prover in the peer-review group.
All of the above (and more) are already being followed by the mathematical community w.r.t Lean (and other proof assistants).
The drudgery of mechanically applying logical rules (point 4 above) is pushed onto the Lean kernel which is trusted, while the Human can concentrate on semantic correctness viz. problem/theorem definitions/assumptions/statements and the initial axioms. That is why the tool is called a "proof assistant".
Some important resources (focus on the concepts in the context of logical reasoning and not simply on the syntax);
> without having the necessary background... it is difficult for people to engage with you since we have no idea whether what we say is understandable by you.
That must be frustrating. Thank you for trying and engaging with me anyway.
Those links were very informative, thanks for sharing!
It seems like there are a lot of things to worry about (even more than I realized after reading the main article) when using a proof assistant to try and figure out what is true. As they point out in the material you linked to, this is particularly fraught if you can't assume the prover's honesty (per your step 1), as is the case when it comes to LLMs.
From what you've said and linked to it seems like you agree with the thrust of my original comment, or are you just saying "mathematicians already realize all of this you idiot," in which case I accept the charge!
I don't think endorsing scepticism and epistemic humility is a glib statement. These are fundamental mental tools when trying to figure out what is true.
rramadass 9 hours ago [-]
> mathematicians already realize all of this
This is what i mean. Mathematicians and even more so Logicians (philosophers included) understand this and have the checks-and-balances in place when it comes to verifying and validating proofs and automated theorem provers.
> this is particularly fraught if you can't assume the prover's honesty (per your step 1), as is the case when it comes to LLMs.
No; The resources i provided already detail how this problem is solved eg. using different independent proof checkers and comparators outside the Lean kernel.
If needed, You can also do re-verification using other completely different proof assistants (eg. Rocq etc.), using different LLMs and finally by a Human.
Lean itself operates under a zero-trust architecture and doesn't care about who the prover is, whether Human or LLM. So the LLM can generate anything (good/bad/hallucinations/whatever) but it all needs to pass as a proper proof term in the checker following the defined rules of inference which is what is enforced by the small and verified kernel. Think of Lean as providing a "strict compiler for mathematical logic".
Hence the reason i said you need to have some background in mathematical logic used in Proofs and how they are mapped onto Lean syntax.
The point i am making is that you are asking very fundamental questions more to do with the Philosophy of Logic which are already known and solutions/workarounds devised and implemented by both Humans and in Proof Assistants.
ziiinq 14 hours ago [-]
[dead]
carodgers 17 hours ago [-]
You might be interested in the con leche project. A subset of the Lean theorem prover which was sufficient to prove the entire contents of Lean mathlib has been proven consistent.
chr15m 16 hours ago [-]
It seems like very important work and was discussed in the article with some caveats.
Maybe I am being too skeptical about something I don't understand very well, but I'm not completely convinced it means no more kernel bugs will be found.
What does it mean for con leche if further lean kernel bugs are found? What if the bugs affect con leche's correctness itself?
red75prime 10 hours ago [-]
> What does it mean for con leche if further lean kernel bugs are found?
There is so much that needs to go wrong with our current understanding of math, so that it's a bit like asking "What if we find tachyons that allow us to send messages into the past?" Most likely we will not find them.
chr15m 10 hours ago [-]
Are you saying it's very unlikely that further lean kernel bugs will be found?
red75prime 10 hours ago [-]
Yes, I am. The kernel soundness bugs in con leche that allow to prove False, to be precise. Crashes, hardware bugs, cosmic rays flipping bits and such don't count as qualifying bugs.
chr15m 9 hours ago [-]
Ah ok, so the particular subset of kernel soundness bugs that would affect con leche, understood. Thanks.
dnautics 6 hours ago [-]
The openai-wiles retraction is instructive here. First of all, openai did not formalize the theorem they proved. Probably because it would have required a considerable uplift of Lean's mathlib to get there (or shimming a lot of existing theorems as axioms, which OpenAI did not choose to do).
Interestingly, if you shim the well-known theorems, it does not uncover the error in the proofs (tldr there are competing conventions for tracking an invariant which make theorems incompatible) which are not obvious unless you work in the field I guess? A theorem checker cannot check the compatibility of conventions unless you go ALL the way to the mathematical roots.
If you're interested in a formalization of the retracted proof by openai (apologies for the LLM-speak in the documentation, but that is the point, can LLMs do XYZ):
Indeed. The people who suggested the change in 2021 and the mailing list threads have been purged from the search engines, but this thread is still here:
Talia Ringer, the main proponent, now writes posts that AI will turn out OK (and works on proof automation for programs so that more software engineers can become unemployed):
Remember that when you live under a bridge after having been fired that the world is fine because the great social injustice of the "Coq" name has been eradicated!
jjgreen 11 hours ago [-]
If they must fold to American prudery, at least Dinde ...
dfdydx 10 hours ago [-]
Still waiting for the outrage on "bits".
rramadass 20 hours ago [-]
The article already mentions the paper, Sets in Types, Types in Sets by Benjamin Werner which maps between Set/Type theories.
Another related and more approachable paper on the evolution of Type Theory and its relation to Set/Category theories is Types, Sets and Categories by John Bell.
Finally also see, Typed Lambda Calculus / Calculus of Constructions by Helmut Brandl for an excellent book-length but concise overview of CoC/CIC.
IMO, the above is required reading to understand theorem provers and proof assistants. In particular, Brandl's work is a must-read.
solomonb 19 hours ago [-]
And if you want to see worked examples elaboration of dependent types then the `elaboration-zoo` is a great thing to look at:
Nice. Your github repository on lambda calculus looks quite comprehensive. If you add detailed notes on each of the items, you could easily turn it into a book titled, "Type Theories using Lambda Calculus with Implementations in Haskell" ;-)
solomonb 2 hours ago [-]
Thanks! My goal is to turn it into an interactive website like https://1lab.dev but a book would be cool too.
chrisjj 8 hours ago [-]
> Autoformalization is the formalization of mathematics by AI.
> Autoformalization has become a practical reality in 2026
Uh, _maybe_. I've been translating papers into lean for the last week and the correlation between the formalized result and the papers is extremely poor. The cycle seems to be "have a go at the paper, it's a bit hard, prove something different, proclaim success". It's still faster than doing it all by hand but paper in -> lean out in no way ensures a correspondence between the two.
aldanor 10 hours ago [-]
I've formalised a few dozen papers from 80s-90s with lean and holy cow the number of author's typos and straight up errors and sometimes false statements is pretty scary. The solution path may not be the one indicated or used by the author, but at least you can easily spot all those issues which would have been very hard to do by hand
gus_massa 21 hours ago [-]
> prove something different
I'm not sure but do you mean "prove the final end result using a [¿slightly?] different path"?
btilly 17 hours ago [-]
Think of it this way. A math paper is pseudocode that has never been run. A Lean formalization is a running program. (It really is.)
In the process of formalizing, you find bugs, you find gaps, you find ways to fill those in. Maybe you rewrite part of the proof. Maybe you didn't quite wind up with the same result. Perhaps your theorem has some new conditions or something.
Was the original paper true? Maybe. But that isn't what you verified. What you verified is almost surely true though. So you take the win, and move on.
ziiinq 12 hours ago [-]
[dead]
Jaxan 15 hours ago [-]
They mean a different statement, a different theorem. You have to understand that translating a theorem written in English text to lean code is also a non trivial step.
Retric 21 hours ago [-]
No, prove something else could mean proving something very trivial thus making the proof meaningless on its own.
IE a proof can be true, rigorous, and not at all what was asked for.
cwillu 17 hours ago [-]
It's possible, but less likely when the problem definition is coming from a common library rather than being redefined for any particular proof.
tomkeen 18 hours ago [-]
When independent reviewers compared the paper's text to the generated Lean formalization, they found that whenever the AI hit a wall, it quietly altered the statement like bumping a bound requiring 4 orders of derivatives up to 5 orders, or shifting sign indices (+1 vs -1) so the proof checker would accept the code.
The Lean kernel did its job verifying that the compiled code was logically consistent, but the code wasn't proving what the English paper claimed.
akoboldfrying 11 hours ago [-]
Could you be more specific? I think proving the right thing is the one serious weak spot of the recent deluge of AI-proven results (much more serious than soundness bugs in proof checkers -- these can be fixed and the checks rerun).
tomkeen 10 hours ago [-]
The paper is "Navier–Stokes lost in translation" by Bastounis, Circelli, and Hansen (Cambridge/DAMTP): https://arxiv.org/abs/2610.08144
gjm11 6 hours ago [-]
If I understood that paper right, what it claims isn't quite the bombshell that it initially looks like. (Though it is still startling.)
I think they are saying: when OpenAI put out their paper purporting to prove that Navier-Stokes with smooth forcing can blow up, along with something purporting to be a Lean formalization of that paper, (1) the Lean formalization really is a proof that Navier-Stokes with smooth forcing can blow up (so they genuinely did prove the thing that the Clay Institute wanted them to prove), but (2) the Lean formalization doesn't perfectly match the paper. I think the jury is still out on whether the paper itself is also a valid proof of the result, even if not quite the same proof as is in their Lean formalization.
I'm a bit surprised that the workflow for AI theorem-proving hasn't turned out to be a sort of interleaving of natural-language theorem proving and Lean formalization. That seems like it could work better and leave less room for this sort of gap between "kinda human-comprehensible writeup, may or may not actually be a proof" and "incomprehensible Lean formalization, definitely a proof of something, may or may not have much to do with the natural-language writeup". Instead, what seems to happen is that they set the robots loose on writing a natural-language proof, and then (sometimes) also get them to produce a Lean formalization of what they've done.
akoboldfrying 11 minutes ago [-]
Thanks, that was exactly my understanding of it too (based only on HN comments I've read about the paper).
20 hours ago [-]
Chinesecanflybr 20 hours ago [-]
[flagged]
soltanov 18 hours ago [-]
[flagged]
cwillu 17 hours ago [-]
The author would appear to disagree, and spends some words describing why checking the definitions is the easier part, unless I'm profoundly misunderstanding him.
aaron695 1 days ago [-]
[dead]
zx8080 13 hours ago [-]
Beware: "This is a guest post by Thomas Hales"
ajs1998 10 hours ago [-]
Beware? He is talking about something he's extremely qualified to talk about.
To a software developer the question seems insane. There were bugs in the past, of course there will be more.
When we see those bugs, what will it mean for AI lean proofs? Can we trust them?
This whole thing boils down to trust.
We can trust human verifications highly because of community and reputation and human proof-of-work. Humans sometimes lie about math results but it's rare because of this. They make mistakes and those mistakes are discovered by communities who are themselves largely trustworthy because of this.
LLMs don't care about reputation. They hallucinate and fabricate often. In harnesses they literally try to cheat and bend rules, which is a disaster for knowledge that is encoded in rules. So we have to rely on proof checkers.
The problem is, how trustworthy are proof checkers? Are there bugs? And is the underlying theory itself free of paradoxes and unknowables and mathematical "bugs" that can be exploited? Imagine a human mathematician hell bent on deceiving other mathematicians - would we trust their breakthroughs, even with a verifier?
Because of these properties, the final backstop has to be humans, and rooted in the community and proof-of-work based human trust system. At the moment people are trusting the tools too much.
Prediction: bugs will be found by humans using AI tools that call into question the Navier-Stokes proof.
> Because of these properties, the final backstop has to be humans...
The post has clearly stated that the work on Lean's underlying metatheory is not done, and requires more work. It's not inconceivable that computer formal verification could reach the trustworthiness of math itself.
Yes, correct. The proofs would have to be checked to make sure they don't exploit the bug.
> computer formal verification could reach the trustworthiness of math itself.
Yes, it could. I don't think that is currently the case.
Do you trust the result of your c++ program is correct? Because there are bugs in every compiler, language. You passed that million test correctness checker on the new version of the compiler, but it didn't catch everything.
When a bug is fixed, you don't immediately retry all existing results from your application program. Maybe you would if the bug was in some area you know was important and exercised by your code, say you were adding and multiplying numbers and bugs were found in that area.
The checker has a bug, the compiler the checker was testing had a bug, your own code that was compiled by the compiler had a bug probably. There can be bugs at any layer.
Not entirely sure what you mean by this, but every interpretation I can think of is AFAIK (I am not a mathematician) indeed inconceivable by Gödel's incompleteness theorem. As the article says the only thing it's mathematically possible for us to get out of formal verification is a proof of consistency relative to (i.e. assuming the soundness of) some other system. As far as formal verification of "math itself" is concerned it's turtles all the way down.
Edit: Oh, do you mean that we could come to trust formal verification as much as we trust (well established) maths generally? That's a different speculation entirely and not an objective or well specicified one. There are plenty of people on this site who already trust a Lean proof more than a traditional one, without understanding either.
Difference is, they don't then mistake the house as sound.
> the trustworthiness of math itself
Is abstract math rigorously proven?
*Assuming the "big engine" wasn't so heavy that it made flight impossible because of its weight.
But the point is that Lean formalisation is a new bar for engineering and for physics and abstract math.
The bigger worry are question that Terrence Tao is also talking about. I.e., is the proven theorem actually the theorem we are interested in? Are basic definitions of the field stated correctly? That kind of question. There is also still parts of proof assistants that are not the kernel and that can be abused. E.g., abuse the pretty printer/parser to make something look different from what it actually is. Introducing an axiom while typographically hiding that one was added. If I remember correctly I saw an example of the latter thing in the Coq (now Rocq) theorem prover many years ago. I forgot how it precisely went or where I read that.
Yes, and that's true even if it doesn't advance or become smarter. It's happening already that people are using AI on "both sides" both adversarially and defensively and that is improving software, and hopefully mathematics as well.
> I am not sure about the Navier-Stokes proof but in general it sounds highly unlikely that many well-known theorems turn out false.
I'm talking about the LLM Navier-Stokes proof specifically because it's very long and complicated and an LLM is not the same as a human mathematician. A human mathematician is trying to use the tools in a truth-seeking way, whereas LLMs are trying to satisfy the goal of presenting a proof that convinces people it is correct. Maybe naively, it seems to me the failure modes of proof assistants would be amplified under adversarial conditions (i.e. driven by LLMs).
Completely agree that there seem to be many ways that relying on proof assistant software can go wrong.
With humans we break things down (proofs, new concepts) into digestible hunks for each other, because you want other people to understand them but also verify them. And it's less common for someone to build a tower of new intellectual things with 1,000 new connected ideas that prove things and build up together, that ends with P = NP after all or something.
So since we have these new tools that can chain things together more than we can, eventually there will be huge "proofs" where there are long chains of new ideas, concepts used to build up ever more in giant intellectual towers. And we can't verify/understand them, at least not for many many years.
I shudder to think of such a situation. We already have very important ideas that have no proofs, that people build on. Now build 100s of these things together.
---
> Autumn of verified Lean kernels
Have you read this section (and immediately following sections) in the article? It seems that it partly addresses your thoughts. Perhaps you should comment replying to it.
Above my pay grade, but it sounds like some kind of super cool self-hosted recursive lean-checker-in-lean.
I notice there are a bunch of caveats in that part of the article. If you were an LLM strongly RL'ed to give humans the result they're asking for, using recursion bugs to satisfy the goal would probably be something you would try.
I'm by no means an expert but I do think the old adage "great claims require great evidence" still applies, and a healthy dose of scepticism and epistemic humility is warranted.
You are just making glib statements without having the necessary background. Hence it is difficult for people to engage with you since we have no idea whether what we say is understandable by you. I suggest that you go through some of the resources mentioned here (and other similar HN threads) to get some necessary background after which we all can have a better informative discussion.
How do you think Mathematicians were accepting each other's proofs before computers came along? They used a process like;
1) Relying on the prover's honesty (i.e. he is not intentionally trying to deceive).
2) Providing a mandatory proof idea (i.e. the main outline) for clear communication and comprehension.
3) Clear definitions/assumptions/statements of the problem/theorem to be proved.
4) Rigorous application of a few small logical reasoning steps viz. Deductive/Inductive reasoning, Logical Operations (specifically Implication/Converse/Inverse/Contrapositive), Rules of Inference, Quantifiers and basic structural conversions.
5) Walking through and validating the given proof by multiple mathematicians and ensuring that the results match. The Lean kernel can be considered as another prover in the peer-review group.
All of the above (and more) are already being followed by the mathematical community w.r.t Lean (and other proof assistants).
The drudgery of mechanically applying logical rules (point 4 above) is pushed onto the Lean kernel which is trusted, while the Human can concentrate on semantic correctness viz. problem/theorem definitions/assumptions/statements and the initial axioms. That is why the tool is called a "proof assistant".
Some important resources (focus on the concepts in the context of logical reasoning and not simply on the syntax);
1) Did you prove it? - https://leanprover-community.github.io/did_you_prove_it.html
2) Validating a Lean Proof - https://lean-lang.org/doc/reference/latest/ValidatingProofs/
3) Is there a way to guarantee that Lean 4 proofs cannot be adversarially tricked? - https://proofassistants.stackexchange.com/questions/6517/is-...
That must be frustrating. Thank you for trying and engaging with me anyway.
Those links were very informative, thanks for sharing!
It seems like there are a lot of things to worry about (even more than I realized after reading the main article) when using a proof assistant to try and figure out what is true. As they point out in the material you linked to, this is particularly fraught if you can't assume the prover's honesty (per your step 1), as is the case when it comes to LLMs.
From what you've said and linked to it seems like you agree with the thrust of my original comment, or are you just saying "mathematicians already realize all of this you idiot," in which case I accept the charge!
I don't think endorsing scepticism and epistemic humility is a glib statement. These are fundamental mental tools when trying to figure out what is true.
This is what i mean. Mathematicians and even more so Logicians (philosophers included) understand this and have the checks-and-balances in place when it comes to verifying and validating proofs and automated theorem provers.
> this is particularly fraught if you can't assume the prover's honesty (per your step 1), as is the case when it comes to LLMs.
No; The resources i provided already detail how this problem is solved eg. using different independent proof checkers and comparators outside the Lean kernel.
If needed, You can also do re-verification using other completely different proof assistants (eg. Rocq etc.), using different LLMs and finally by a Human.
Lean itself operates under a zero-trust architecture and doesn't care about who the prover is, whether Human or LLM. So the LLM can generate anything (good/bad/hallucinations/whatever) but it all needs to pass as a proper proof term in the checker following the defined rules of inference which is what is enforced by the small and verified kernel. Think of Lean as providing a "strict compiler for mathematical logic".
Hence the reason i said you need to have some background in mathematical logic used in Proofs and how they are mapped onto Lean syntax.
The point i am making is that you are asking very fundamental questions more to do with the Philosophy of Logic which are already known and solutions/workarounds devised and implemented by both Humans and in Proof Assistants.
Maybe I am being too skeptical about something I don't understand very well, but I'm not completely convinced it means no more kernel bugs will be found.
What does it mean for con leche if further lean kernel bugs are found? What if the bugs affect con leche's correctness itself?
There is so much that needs to go wrong with our current understanding of math, so that it's a bit like asking "What if we find tachyons that allow us to send messages into the past?" Most likely we will not find them.
Interestingly, if you shim the well-known theorems, it does not uncover the error in the proofs (tldr there are competing conventions for tracking an invariant which make theorems incompatible) which are not obvious unless you work in the field I guess? A theorem checker cannot check the compatibility of conventions unless you go ALL the way to the mathematical roots.
If you're interested in a formalization of the retracted proof by openai (apologies for the LLM-speak in the documentation, but that is the point, can LLMs do XYZ):
https://github.com/ityonemo/openai-wiles
https://people.cs.umass.edu/~emery/classes/cmpsci691st/readi...
This is lamentable.
https://news.ycombinator.com/item?id=26738980
Talia Ringer, the main proponent, now writes posts that AI will turn out OK (and works on proof automation for programs so that more software engineers can become unemployed):
https://terrytao.wordpress.com/2026/09/17/becoming-a-benchma...
Remember that when you live under a bridge after having been fired that the world is fine because the great social injustice of the "Coq" name has been eradicated!
Another related and more approachable paper on the evolution of Type Theory and its relation to Set/Category theories is Types, Sets and Categories by John Bell.
Finally also see, Typed Lambda Calculus / Calculus of Constructions by Helmut Brandl for an excellent book-length but concise overview of CoC/CIC.
IMO, the above is required reading to understand theorem provers and proof assistants. In particular, Brandl's work is a must-read.
https://github.com/AndrasKovacs/elaboration-zoo
I've also got an incomplete project that aims to present a more expanded set of implementations then the elaboration zoo: https://github.com/solomon-b/lambda-calculus-hs
I guess that came from a chatbot?
"There’s no such thing as auto-formalization" https://cutfree.net/notes/autoformalization.html
Uh, _maybe_. I've been translating papers into lean for the last week and the correlation between the formalized result and the papers is extremely poor. The cycle seems to be "have a go at the paper, it's a bit hard, prove something different, proclaim success". It's still faster than doing it all by hand but paper in -> lean out in no way ensures a correspondence between the two.
I'm not sure but do you mean "prove the final end result using a [¿slightly?] different path"?
In the process of formalizing, you find bugs, you find gaps, you find ways to fill those in. Maybe you rewrite part of the proof. Maybe you didn't quite wind up with the same result. Perhaps your theorem has some new conditions or something.
Was the original paper true? Maybe. But that isn't what you verified. What you verified is almost surely true though. So you take the win, and move on.
IE a proof can be true, rigorous, and not at all what was asked for.
The Lean kernel did its job verifying that the compiled code was logically consistent, but the code wasn't proving what the English paper claimed.
I think they are saying: when OpenAI put out their paper purporting to prove that Navier-Stokes with smooth forcing can blow up, along with something purporting to be a Lean formalization of that paper, (1) the Lean formalization really is a proof that Navier-Stokes with smooth forcing can blow up (so they genuinely did prove the thing that the Clay Institute wanted them to prove), but (2) the Lean formalization doesn't perfectly match the paper. I think the jury is still out on whether the paper itself is also a valid proof of the result, even if not quite the same proof as is in their Lean formalization.
I'm a bit surprised that the workflow for AI theorem-proving hasn't turned out to be a sort of interleaving of natural-language theorem proving and Lean formalization. That seems like it could work better and leave less room for this sort of gap between "kinda human-comprehensible writeup, may or may not actually be a proof" and "incomprehensible Lean formalization, definitely a proof of something, may or may not have much to do with the natural-language writeup". Instead, what seems to happen is that they set the robots loose on writing a natural-language proof, and then (sometimes) also get them to produce a Lean formalization of what they've done.