4 ms·

You absolutely need to read the lean proof firstly to assess the correctness of the proposition it is proving (ie in this case that it is actually proving or ot

You absolutely need to read the lean proof firstly to assess the correctness of the proposition it is proving (ie in this case that it is actually proving or otherwise the smoothness of navier-stokes in R^3 and not something else) and secondly to determine whether the proof is “honest” in the sense given here https://lean-lang.org/doc/reference/latest/ValidatingProofs/ https://lean-lang.org/doc/reference/latest/ValidatingProofs/

zone411 21d ago
Completely misleading. This is all you need to read and understand for Anthropic's FLT formalization: import Mathlib import Theorems.Thm_fermat_last_theorem /-- Solution side: the same statement, binder for binder, proved by this tree's `fermat_last_theorem`. -/ theorem FLT_for_comparator (n : ℕ) (hn : 3 ≤ n) (a b c : ℕ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : a ^ n + b ^ n ≠ c ^ n := fermat_last_theorem n hn a b c ha hb hc /-- Mathlib's named proposition, by the one-line bridge from the elementary statement (the bridge is restated inline so that this file depends only on `Theorems.Thm_fermat_last_theorem`). -/ theorem FLT_mathlib_for_comparator : FermatLastTheorem := fun n hn a b c ha hb hc => fermat_last_theorem n hn a b c (Nat.pos_of_ne_zero ha) (Nat.pos_of_ne_zero hb) (Nat.pos_of_ne_zero hc) The actual proof is 13 million lines of Lean.
- u1hcw9nx 21d ago
  Lean roof search tactics can generate vacuous proofs. They are not errors or a degenerate cases. They are completely valid, sound proof terms. Building a system that reliably detects vacuous proofs in all cases is fundamentally undecidable. It's equal to the halting problem.
  - i_no_can_eat 21d ago
    Can you elaborate on what constitutes a vacuous proof?
    - JumpCrisscross 21d ago
      > Can you elaborate on what constitutes a vacuous proof? Trivially, a proof that relies on a bug in Lean. Less trivially, a proof that is technically true but about something trivial and does not, in fact, prove what it claims to have proven.
    - Tanjreeve 21d ago
      I present to you my new theorem as follows: If 1 == 3 then 3 == 3 ---- This statement is 100% logically coherent internally. But it also doesn't matter because we know that 1 does not equal 3 so this proof is completely pointless. I could also say 3 == 5 and it would still be logically sound but completely useless information.
      - Panzer04 21d ago
        For a laymen, I don't follow this. Are you proving for some arbitrary definition of == that isn't what we commonly consider the definition? How is it logically coherent? You mean only in the sense that you say it is and you haven't provided any rules to disprove it?
        JumpCrisscross 21d ago
        > How is it logically coherent? It's not. But Lean doesn't interrogate logical coherence, just internal consistency.
        NewsaHackO 21d ago
        No the definition of == is the regular definition; it's just a deductive reasoning statement. Since the first part of the statement is never true, it doesn't matter what the second part of it says. Of course, like he said, that makes the statement have no value.
        paulddraper 21d ago
        “if X then Y” means “(not X) or Y” E.g. “If it’s raining, the sidewalk is wet.” That statement holds if it’s not raining or the sidewalk is wet. This is a common occurrence in mathematics, where someone might not be able to unconditionally prove Y, but they can under the condition X. Later, another mathematician might build on this by proving X, thereby transitively proving Y. (Or conversely, they might unconditionally disprove Y, thereby disproving X.) Many hard problems are answered this way. For example, Fermat’s Last Theorem was proven assuming the Taniyama-Shimura-Weil Conjecture, then Wiles proved the conjecture. Thousands of theorems rely on the the unproven Reinmann Hypothesis, which is why it’s so interesting to mathematicians. But if your precondition is “stupid,” your proof is stupid.
- Paracompact 21d ago
  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 21d 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 21d 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 21d 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 21d 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 21d ago
eru 21d ago
You don't need to read the lean proof for that, only the statement.
- seanhunter 21d ago
  You need to read the lean proof (not just the statement of the proposition) to assess whether the proof is honest. The link I provided is the lean prover community firstly officially agreeing with that claim and secondly explaining why that is the case.
  - eru 21d ago
    Well, Lean needs to get its act together to fix the bugs.
    - seanhunter 20d ago
      They’re working on it, but the bulk of the effort goes into making it more useful to working mathematicians rather than resisting malicious proof attempts.
hn_throwaway_99 21d ago
While I agree with that, my layman's understanding is that the whole purpose of Lean is that once you agree that the program does "do what it says it does", all the intermediate steps can be verified with a compilation. That is, verifying a proof in English was a painstaking, years long process in the past as independent mathematicians looked for holes in the steps connecting the logic. When the proof is written in Lean, all of that work goes away. My point is that if OpenAI publishes the Lean code (not sure if they already did), verification should take weeks not years.

zone411 21d ago

Completely misleading. This is all you need to read and understand for Anthropic's FLT formalization: import Mathlib import Theorems.Thm_fermat_last_theorem /-- Solution side: the same statement, binder for binder, proved by this tree's `fermat_last_theorem`. -/ theorem FLT_for_comparator (n : ℕ) (hn : 3 ≤ n) (a b c : ℕ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : a ^ n + b ^ n ≠ c ^ n := fermat_last_theorem n hn a b c ha hb hc /-- Mathlib's named proposition, by the one-line bridge from the elementary statement (the bridge is restated inline so that this file depends only on `Theorems.Thm_fermat_last_theorem`). -/ theorem FLT_mathlib_for_comparator : FermatLastTheorem := fun n hn a b c ha hb hc => fermat_last_theorem n hn a b c (Nat.pos_of_ne_zero ha) (Nat.pos_of_ne_zero hb) (Nat.pos_of_ne_zero hc) The actual proof is 13 million lines of Lean.

u1hcw9nx 21d ago
Lean roof search tactics can generate vacuous proofs. They are not errors or a degenerate cases. They are completely valid, sound proof terms. Building a system that reliably detects vacuous proofs in all cases is fundamentally undecidable. It's equal to the halting problem.
- i_no_can_eat 21d ago
  Can you elaborate on what constitutes a vacuous proof?
  - JumpCrisscross 21d ago
    > Can you elaborate on what constitutes a vacuous proof? Trivially, a proof that relies on a bug in Lean. Less trivially, a proof that is technically true but about something trivial and does not, in fact, prove what it claims to have proven.
  - Tanjreeve 21d ago
    I present to you my new theorem as follows: If 1 == 3 then 3 == 3 ---- This statement is 100% logically coherent internally. But it also doesn't matter because we know that 1 does not equal 3 so this proof is completely pointless. I could also say 3 == 5 and it would still be logically sound but completely useless information.
    - Panzer04 21d ago
      For a laymen, I don't follow this. Are you proving for some arbitrary definition of == that isn't what we commonly consider the definition? How is it logically coherent? You mean only in the sense that you say it is and you haven't provided any rules to disprove it?
      - JumpCrisscross 21d ago
        > How is it logically coherent? It's not. But Lean doesn't interrogate logical coherence, just internal consistency.
      - NewsaHackO 21d ago
        No the definition of == is the regular definition; it's just a deductive reasoning statement. Since the first part of the statement is never true, it doesn't matter what the second part of it says. Of course, like he said, that makes the statement have no value.
      - paulddraper 21d ago
        “if X then Y” means “(not X) or Y” E.g. “If it’s raining, the sidewalk is wet.” That statement holds if it’s not raining or the sidewalk is wet. This is a common occurrence in mathematics, where someone might not be able to unconditionally prove Y, but they can under the condition X. Later, another mathematician might build on this by proving X, thereby transitively proving Y. (Or conversely, they might unconditionally disprove Y, thereby disproving X.) Many hard problems are answered this way. For example, Fermat’s Last Theorem was proven assuming the Taniyama-Shimura-Weil Conjecture, then Wiles proved the conjecture. Thousands of theorems rely on the the unproven Reinmann Hypothesis, which is why it’s so interesting to mathematicians. But if your precondition is “stupid,” your proof is stupid.
Paracompact 21d ago
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 21d 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 21d 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 21d 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 21d 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 21d ago

eru 21d ago

You don't need to read the lean proof for that, only the statement.

seanhunter 21d ago
You need to read the lean proof (not just the statement of the proposition) to assess whether the proof is honest. The link I provided is the lean prover community firstly officially agreeing with that claim and secondly explaining why that is the case.
- eru 21d ago
  Well, Lean needs to get its act together to fix the bugs.
  - seanhunter 20d ago
    They’re working on it, but the bulk of the effort goes into making it more useful to working mathematicians rather than resisting malicious proof attempts.

hn_throwaway_99 21d ago

While I agree with that, my layman's understanding is that the whole purpose of Lean is that once you agree that the program does "do what it says it does", all the intermediate steps can be verified with a compilation. That is, verifying a proof in English was a painstaking, years long process in the past as independent mathematicians looked for holes in the steps connecting the logic. When the proof is written in Lean, all of that work goes away. My point is that if OpenAI publishes the Lean code (not sure if they already did), verification should take weeks not years.