5 ms·

Can someone with more knowledge help me with this silly question in my head? >>Along the way, it wrote 13 million lines of Lean and proved 29,500 intermediate

by prometheus1992 12d ago

Can someone with more knowledge help me with this silly question in my head? >>Along the way, it wrote 13 million lines of Lean and proved 29,500 intermediate theorems Did a human check the 13 million lines of code? How does QA'ing this type of work works?

hyperhello 12d ago
The point of writing Lean code is that Lean checks it accordingly. Lean is a domain specific language to encode mathematical reasoning in a way that can’t be fooled. Note to other users: don’t downvote this kind of comment, answer it.
- epgui 12d ago
  Is Lean a DSL? I’d argue it’s a general purpose programming language that excels at proofs.
  - hyperhello 12d ago
    Well, there’s actually a very small set of operations that allow all computation, so it doesn’t take much to be a DSL and a GP too; I’d be surprised if a proof language couldn’t swing it.
  - mswphd 12d ago
    it is a general-purpose programming language. for example, it's standard library allows you to do file io, networking, etc.
- stratos123 12d ago
  encode mathematical reasoning in a way that can’t be fooled. I would be a bit careful asserting that in full generality, given https://github.com/James-Hanson/junk-theorems-in-lean https://github.com/James-Hanson/junk-theorems-in-lean
  - hyperhello 12d ago
    Isn’t there some theorem that any sufficiently complex mathematical languages will have statements that can’t be proven? :)
    - fn-mote 12d ago
      This would be funny if it were relevant. Seems like a statement about false negatives instead of false positives. False negative = could not find a proof of a true theorem. False positive = erroneous proof of a theorem.
  - mswphd 12d ago
    junk theorems aren't the concern, soundness issues in the lean kernel are the concern. Notably, junk theorems are true. Nobody would debate that the junk theorem is true. The main thing people would say is that junk theorems, while being true, are sensitive to precisely how you encoded mathematics, so despite being true, they are perhaps not conceptually meaningful. As an example of a junk theorem, sasy you use the definition of the natural numbers using von neumann ordinals https://en.wikipedia.org/wiki/Set-theoretic_definition_of_natural_numbers https://en.wikipedia.org/wiki/Set-theoretic_definition_of_na... Then for any natural numbers n, m, they're implicitly sets. So n \intersect m = min(n,m). This is the wrong way to think about natural numbers. You should not use this ever in proofs. But this isn't because your proofs would be false, but instead because it is a fundamentally confusing way to think about the natural numbers. It is in this sense it is a "junk theorem".
  - ndriscoll 12d ago
    This has nothing to do with Lean, e.g. > The first coordinate of the polynomial X^2 (X^3 + X + 1 ) is equal to the prime factorization of 30 . We defined polynomials as their coefficient functions in my algebra class, and it makes sense that you'd define a prime factorization as a function from primes to N, which naturally extends to a function N->N. So this junk theorem is part of normal math too. It just says in an obtuse way that they're both the function that's 1 at 2, 3, and 5, and 0 elsewhere.
  - kzrdude 11d ago
fwip 12d ago
The nice thing about theorem provers is that you don't need to read the intermediate lines. You need to make sure that the goal/result actually matches what you think it says - but everything in the middle is validated by the prover.
babelfish 12d ago
A human definitely didn't, but one of the benefits of formal verification is that even if the work done to achieve something is slop-y or excessively verbose, solvers like Lean guarantee that the initial proposition (assuming it was written correctly and in this case was definitely reviewed by humans) is definitively True. This is true across other domains of formal verification outside of math as well
- bobmarleybiceps 12d ago
  guaranteed, up to lean itself having bugs that are exploited by the LLM :shrug:
  - CaptWorld 12d ago
    Do you have proof of this bug or something? Is this just envy against computers now ?
    - mswphd 12d ago
      as mentioned elsewhere, there was a bug in the lean kernel exploited by AI to prove a false statement roughly a month ago https://leodemoura.github.io/blog/2026-8-1-postmortem-for-kernel-soundness-bug-14576/ https://leodemoura.github.io/blog/2026-8-1-postmortem-for-ke...
      - CaptWorld 12d ago
        Got it. Thanks. I feel people are using this single story to downplay this feat. There's definitely a chance but I don't see any indication of similar bugs in here or the openai's proofs that were created a month ago as i think these companies might've vetted it enough and the other team who's working on similar lean proof for this also seems to have acknowledged this feat
        bobmarleybiceps 12d ago
        [dead]
stabbles 12d ago
There is a simple piece of code that can check simple steps, and many people agree this checker is correct. Then there is a formalization of the theorem which many people agree defines the theorem accurately. Then there is 13 million lines of proof that nobody has read, but the proof checker validated each step. That's enough. So, all you have to verify is the formalization of the theorem, and believe that the proof checker is free of bugs. You don't have to read the actual proof.
- Jblx2 12d ago
  You still have to trust that the AI didn't exploit a bug in the Lean kernel. There was just such an instance of a bug a little over a month ago: https://leodemoura.github.io/blog/2026-8-1-postmortem-for-kernel-soundness-bug-14576/ https://leodemoura.github.io/blog/2026-8-1-postmortem-for-ke...
  - vessenes 12d ago
    True, .. and. In this case, the original proof is considered rigorously checked, so finding a bug in the kernel would be nice to know about, but in my opinion would not take away from the accomplishment (FLT in lean using agents) nor the many benefits of getting these mathematical objects formalized and usable in Lean in the future.
lordnacho 12d ago
This was my question as well. The way I understand it, it's like a compiler, it implements rules, in this case logic/math rules that tell you whether something follows from assumptions you've given it. But how do you know you told it what you intended to tell it?
tossandthrow 12d ago
No. No human checked it. But a type checker did. And that is much better.

hyperhello 12d ago

The point of writing Lean code is that Lean checks it accordingly. Lean is a domain specific language to encode mathematical reasoning in a way that can’t be fooled. Note to other users: don’t downvote this kind of comment, answer it.

epgui 12d ago
Is Lean a DSL? I’d argue it’s a general purpose programming language that excels at proofs.
- hyperhello 12d ago
  Well, there’s actually a very small set of operations that allow all computation, so it doesn’t take much to be a DSL and a GP too; I’d be surprised if a proof language couldn’t swing it.
- mswphd 12d ago
  it is a general-purpose programming language. for example, it's standard library allows you to do file io, networking, etc.
stratos123 12d ago
encode mathematical reasoning in a way that can’t be fooled. I would be a bit careful asserting that in full generality, given https://github.com/James-Hanson/junk-theorems-in-lean https://github.com/James-Hanson/junk-theorems-in-lean
- hyperhello 12d ago
  Isn’t there some theorem that any sufficiently complex mathematical languages will have statements that can’t be proven? :)
  - fn-mote 12d ago
    This would be funny if it were relevant. Seems like a statement about false negatives instead of false positives. False negative = could not find a proof of a true theorem. False positive = erroneous proof of a theorem.
- mswphd 12d ago
  junk theorems aren't the concern, soundness issues in the lean kernel are the concern. Notably, junk theorems are true. Nobody would debate that the junk theorem is true. The main thing people would say is that junk theorems, while being true, are sensitive to precisely how you encoded mathematics, so despite being true, they are perhaps not conceptually meaningful. As an example of a junk theorem, sasy you use the definition of the natural numbers using von neumann ordinals https://en.wikipedia.org/wiki/Set-theoretic_definition_of_natural_numbers https://en.wikipedia.org/wiki/Set-theoretic_definition_of_na... Then for any natural numbers n, m, they're implicitly sets. So n \intersect m = min(n,m). This is the wrong way to think about natural numbers. You should not use this ever in proofs. But this isn't because your proofs would be false, but instead because it is a fundamentally confusing way to think about the natural numbers. It is in this sense it is a "junk theorem".
- ndriscoll 12d ago
  This has nothing to do with Lean, e.g. > The first coordinate of the polynomial X^2 (X^3 + X + 1 ) is equal to the prime factorization of 30 . We defined polynomials as their coefficient functions in my algebra class, and it makes sense that you'd define a prime factorization as a function from primes to N, which naturally extends to a function N->N. So this junk theorem is part of normal math too. It just says in an obtuse way that they're both the function that's 1 at 2, 3, and 5, and 0 elsewhere.
- kzrdude 11d ago

fwip 12d ago

The nice thing about theorem provers is that you don't need to read the intermediate lines. You need to make sure that the goal/result actually matches what you think it says - but everything in the middle is validated by the prover.

babelfish 12d ago

A human definitely didn't, but one of the benefits of formal verification is that even if the work done to achieve something is slop-y or excessively verbose, solvers like Lean guarantee that the initial proposition (assuming it was written correctly and in this case was definitely reviewed by humans) is definitively True. This is true across other domains of formal verification outside of math as well

bobmarleybiceps 12d ago
guaranteed, up to lean itself having bugs that are exploited by the LLM :shrug:
- CaptWorld 12d ago
  Do you have proof of this bug or something? Is this just envy against computers now ?
  - mswphd 12d ago
    as mentioned elsewhere, there was a bug in the lean kernel exploited by AI to prove a false statement roughly a month ago https://leodemoura.github.io/blog/2026-8-1-postmortem-for-kernel-soundness-bug-14576/ https://leodemoura.github.io/blog/2026-8-1-postmortem-for-ke...
    - CaptWorld 12d ago
      Got it. Thanks. I feel people are using this single story to downplay this feat. There's definitely a chance but I don't see any indication of similar bugs in here or the openai's proofs that were created a month ago as i think these companies might've vetted it enough and the other team who's working on similar lean proof for this also seems to have acknowledged this feat
      - bobmarleybiceps 12d ago
        [dead]

stabbles 12d ago

There is a simple piece of code that can check simple steps, and many people agree this checker is correct. Then there is a formalization of the theorem which many people agree defines the theorem accurately. Then there is 13 million lines of proof that nobody has read, but the proof checker validated each step. That's enough. So, all you have to verify is the formalization of the theorem, and believe that the proof checker is free of bugs. You don't have to read the actual proof.

Jblx2 12d ago
You still have to trust that the AI didn't exploit a bug in the Lean kernel. There was just such an instance of a bug a little over a month ago: https://leodemoura.github.io/blog/2026-8-1-postmortem-for-kernel-soundness-bug-14576/ https://leodemoura.github.io/blog/2026-8-1-postmortem-for-ke...
- vessenes 12d ago
  True, .. and. In this case, the original proof is considered rigorously checked, so finding a bug in the kernel would be nice to know about, but in my opinion would not take away from the accomplishment (FLT in lean using agents) nor the many benefits of getting these mathematical objects formalized and usable in Lean in the future.

lordnacho 12d ago

This was my question as well. The way I understand it, it's like a compiler, it implements rules, in this case logic/math rules that tell you whether something follows from assumptions you've given it. But how do you know you told it what you intended to tell it?

tossandthrow 12d ago

No. No human checked it. But a type checker did. And that is much better.