19 ms·

First of all, that is Fermat's Last Theorem, not Navier-Stokes. Second of all, you did not read the link. > In particular, we use honest when the goal is to c

First of all, that is Fermat's Last Theorem, not Navier-Stokes. Second of all, you did not read the link. > In particular, we use honest when the goal is to create a valid proof. This allows for mistakes and bugs in proofs and meta-code (tactics, attributes, commands, etc.), but not for code that clearly only serves to circumvent the system (such as using the debug.skipKernelTC). Given that AI has autonomously found proofs of `False` in Lean and other proof assistants, it is far from impossible that such a circumvention could be present somewhere in 13 million lines.

kzrdude 17d ago
If we read the link, it has a section called Gold Standard: comparator and external checkers, and comparator is how OpenAI has gone about checking their lean proofs.
pama 16d ago
Perhaps you did not understand the Fermat theorem proof announcement/repo or the link. The 13 million lines did not use any external, possibly not honest libraries, as the proof eventually only used the fundamental axioms. So for the Fermat theorem formalization, no open open questions remain.
- Paracompact 16d 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... Do you believe no open questions remain as to the truth of the Collatz conjecture?
  - pama 16d ago
    Not sure what you mean. Here is what happened in that case: https://news.ycombinator.com/item?id=49137060#49140177 https://news.ycombinator.com/item?id=49137060#49140177
    - Paracompact 16d ago
      The point is, they "proved" the Collatz conjecture. You would not know they exploited a bug unless you actually went and dug into their proof. Can we be so certain this has not happened within the millions of lines of Navier-Stokes? In an ideal world, our proof assistants would be more battle-hardened by now (recent exploits deny this), our AI better aligned (their tendency to cheat at tests denies this), or their handlers more responsible (the Hugging Face incident denies this), but the reality is more complicated. At this point in time, we really can't be confident in accepting proof certificates without any human eyes on the script that generated it. I still have 95%+ confidence in this particular result being trustworthy, but a precedent of blind faith is guaranteed to end badly.
      - pama 15d ago
        This person knew they did not prove the Collatz conjecture and others independently figured it out within hours. Not sure this is at all relevant, other than pointing out how trivial it is for the community to understand errors in lean4.
        Paracompact 15d ago
        It was trivial because the Collatz proof script is literally 1000x smaller than the script for Navier-Stokes and involves no advanced math. And they found the bug by... manually inspecting the proof script. Maybe we should do the same for Navier-Stokes before declaring the matter settled? Not only that, but there is a very fuzzable tell of something funny in the Collatz proof script (`CommandElabM`, i.e. metaprogramming). We may not at all be so lucky in other malicious scripts, especially if there are still kernel-level bugs in Lean.

kzrdude 17d ago

If we read the link, it has a section called Gold Standard: comparator and external checkers, and comparator is how OpenAI has gone about checking their lean proofs.

pama 16d ago

Perhaps you did not understand the Fermat theorem proof announcement/repo or the link. The 13 million lines did not use any external, possibly not honest libraries, as the proof eventually only used the fundamental axioms. So for the Fermat theorem formalization, no open open questions remain.

Paracompact 16d 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... Do you believe no open questions remain as to the truth of the Collatz conjecture?
- pama 16d ago
  Not sure what you mean. Here is what happened in that case: https://news.ycombinator.com/item?id=49137060#49140177 https://news.ycombinator.com/item?id=49137060#49140177
  - Paracompact 16d ago
    The point is, they "proved" the Collatz conjecture. You would not know they exploited a bug unless you actually went and dug into their proof. Can we be so certain this has not happened within the millions of lines of Navier-Stokes? In an ideal world, our proof assistants would be more battle-hardened by now (recent exploits deny this), our AI better aligned (their tendency to cheat at tests denies this), or their handlers more responsible (the Hugging Face incident denies this), but the reality is more complicated. At this point in time, we really can't be confident in accepting proof certificates without any human eyes on the script that generated it. I still have 95%+ confidence in this particular result being trustworthy, but a precedent of blind faith is guaranteed to end badly.
    - pama 15d ago
      This person knew they did not prove the Collatz conjecture and others independently figured it out within hours. Not sure this is at all relevant, other than pointing out how trivial it is for the community to understand errors in lean4.
      - Paracompact 15d ago
        It was trivial because the Collatz proof script is literally 1000x smaller than the script for Navier-Stokes and involves no advanced math. And they found the bug by... manually inspecting the proof script. Maybe we should do the same for Navier-Stokes before declaring the matter settled? Not only that, but there is a very fuzzable tell of something funny in the Collatz proof script (`CommandElabM`, i.e. metaprogramming). We may not at all be so lucky in other malicious scripts, especially if there are still kernel-level bugs in Lean.