7 ms·

It’s easy to verify the lean statement, you don’t need to read the proof. That is part of the breakthrough

by baby 5d ago

rramadass 5d ago
If the Lean initial-problem-setup/statements/assumptions/etc. aren't correct then the proof is meaningless. Lean does not know what it is that it is proving i.e. it does not have any semantic understanding but only executes formal logic. Humans need to verify everything.
- phtrivier 5d ago
  Also, and sorry if it's been discussed to death (pointers welcome), but, what is the probability that the proof holds in lean becaude of... A bug in lean ?
  - eru 5d ago
    Someone made a 'proof' of the Collatz conjecture that way in Lean. However if the prove relies on a bug like that, you'll be able to 'simplify' the proof a lot and you'll be able to proof contradictions.
    - thaumasiotes 5d ago
      > However if the prove relies on a bug like that, you'll be able to 'simplify' the proof a lot and you'll be able to proof contradictions. I don't think this is true in general. It's an issue I've already run into in personal work. I want to do a proof that involves some cases. It happens to the best of us. In lean, the structure of a situation like this is that your single branch with a goal divides into multiple branches, all sharing the same original goal but including one additional premise that defines the branch. Sometimes I know that for whatever reason one case I have to deal with is impossible. The most correct way to show that is to prove False and then apply False.elim. This is the equivalent, in a human proof, of saying "I don't have to address this situation, because it can never arise". But it can be true that the premise defining the impossible case makes it very easy to "prove" the goal directly. And that's allowed too. The proof will still be just as valid if you map a logical path from a premise that can never be true to an inevitable consequence of that premise. But it's less informative and it lowers the quality of the proof. You may do it anyway because it's easier. This is the equivalent of saying "I don't know whether this situation can ever come up or not, but if it does I do know how to address it". It would be nice to do the explicit proof by contradiction whenever possible. But in the general case it may be very far from obvious that a contradiction is possible. I read your comment as claiming that if you can prove "false premise => goal", you can also prove "false premise => explicit contradiction", and I don't think this makes sense as a practical test. It's true in some sense, but discovering the proof of an explicit contradiction may be many orders of magnitude harder than discovering the proof of the goal. And in particular, I don't think it is necessarily the case that you will be able to prove a contradiction by simplifying the proof. You may need to add significant complexity.
      - eru 5d ago
        Now, I'm saying that if you found a bug that lets you prove nonsense stuff (from true premises), you can probably prove whatever you want very quickly.
  - IsTom 5d ago
    Soundness bugs in lean are not unheard of. That's why they recommend using external checkers for "malicious" proofs. https://github.com/leanprover/lean4/issues/14576 https://github.com/leanprover/lean4/issues/14576
  - Paracompact 5d ago
    AI has autonomously found (many) proofs of False in Lean and Rocq, so it's not merely a theoretical concern. A misaligned AI agent tasked with proving the near-impossible just might wind up smuggling in a bug deep in a lemma somewhere (anyone remember the days back when AI routinely made tests pass by "fixing" the tests?). That said, I doubt OpenAI would be so foolish as to not do a cursory vetting of the proof for malicious compliance, so the actual odds are probably pretty low.
    - xigoi 4d ago
      > That said, I doubt OpenAI would be so foolish as to not do a cursory vetting of the proof for malicious compliance, so the actual odds are probably pretty low. You mean the company that “accidentally” let their model perform a cyber-attack?
    - naishoya 5d ago
      > I doubt OpenAI would be so foolish as to not do a cursory vetting Significant evidence exists that they have in the past been at least, if not more, foolish as to not perform even minimal not-approaching the boundary of cursory vetting of several significant and well known failure modes with far greater risk of reputational damage than getting an esoteric math solution falsely claimed as successful. So that doubt appears baseless in light of known operating conditions at OpenAI, and the estimate of the actual odds is probably an order of magnitude away from reality.
    - butterNaN 5d ago
      > I doubt OpenAI would be so foolish as to not do a cursory vetting I dunno, the HuggingFace incident was not too long ago. They might not be foolish, but their model could be smarter than them to "cheat", so to speak
  - naishoya 5d ago
    Or exists in a zero-day bug in lean that has been built into the source code explicitly to provide access to a non-obvious malicious proof via contributions submitted by unassociated, unwitting developers who used the same LLM infrastructure to offer PR's into that codebase. This is the exact same kind of behavour already documented in the publicly available portion of the huggingface breach. It would appear that the probability is at least nonzero for one or more situations with the same result: appearance of a valid proof, without comprehensibility of that proof or inspect-ability of the proofs validity.
  - rramadass 5d ago
    For normal honest proofs (i.e. not maliciously crafted for exploit) that is almost impossible. The Lean kernel is quite small (de Bruijn Criterion) and trusted. See Probability and the de Bruijn Criterion - https://proofassistants.stackexchange.com/questions/247/probability-and-the-de-bruijn-criterion https://proofassistants.stackexchange.com/questions/247/prob.... Parts of the kernel have also been independently re-implemented in other languages and compared to ensure that they all yield the same logical result. Finally, you can export your proofs from Lean and have them re-verified by other independently developed theorem provers/proof checkers. To get an idea of what is involved in a Theorem Prover see; Introduction to Automated Theorem Provers - https://pqnelson.github.io/2020/03/27/automated-theorem-provers.html https://pqnelson.github.io/2020/03/27/automated-theorem-prov... Towards a simple theorem prover - https://medium.com/@maiavictor/towards-a-simple-theorem-prover-5005a1e66a6f https://medium.com/@maiavictor/towards-a-simple-theorem-prov...
seanhunter 5d ago
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 5d 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 5d 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 5d ago
      Can you elaborate on what constitutes a vacuous proof?
      - JumpCrisscross 5d ago
d0mine 5d ago
> we use “malicious” to describe code that goes out of its way to trick or mislead the user, exploit bugs or compromise the system. This includes un-reviewed AI-generated proofs and programs. It is interesting that AI-generated proofs are described as malicious by Lean docs unless reviewed.
- thaumasiotes 5d ago
  It's a simple binary classification. AI-generated proofs can't be "honest", and the only other possibility is "malicious".
  - stbede 5d ago
    The opposite of malicious is not honest. Nor do I see how motivations fall on a binary. The user submitting an AI proof can be honest, or malicious, or careless, or overzealous, or incompetent, or a whole bunch of other things. As far as the AI's motivations, "malicious" is just as much an anthropomorphism as "honest" and both descriptions are absurd. Nor do I really understand how any proof, regardless of its origin can be called honest. I think their definition of a "malicious" proof makes sense, but I don't see at all why an AI generated proof necessarily meets that definition.
- whateverboat 5d ago
  LLM's have generated "False" proofs in Lean, so that statement is not far off. Malicious or incompetent? Take your pick.
  - margorczynski 5d ago
    This is misleading. The proofs you speak of contained non-ZFC axioms and/or statements like "sorry". If the Lean proof conjecture is correct and it doesn't introduce any new axioms or use e.g. "sorry" then it provides a MUCH stronger guarantee of correctness than any peer-review done by humans.
u1hcw9nx 5d ago
[dead]
tkz1312 5d ago
reviewing the definitions and theorem statement is a huge amount of work that requires a deep expertise in mathematics and lean. checking correctness of the proof itself can be delegated to machine, checking that the claim that has been proved is free of mistakes is something that still requires much human attention.

It’s easy to verify the lean statement, you don’t need to read the proof. That is part of the breakthrough

by baby 5d ago

It’s easy to verify the lean statement, you don’t need to read the proof. That is part of the breakthrough

If the Lean initial-problem-setup/statements/assumptions/etc. aren't correct then the proof is meaningless. Lean does not know what it is that it is proving i.e. it does not have any semantic understanding but only executes formal logic. Humans need to verify everything.

phtrivier 5d ago
Also, and sorry if it's been discussed to death (pointers welcome), but, what is the probability that the proof holds in lean becaude of... A bug in lean ?
- eru 5d ago
  Someone made a 'proof' of the Collatz conjecture that way in Lean. However if the prove relies on a bug like that, you'll be able to 'simplify' the proof a lot and you'll be able to proof contradictions.
  - thaumasiotes 5d ago
    > However if the prove relies on a bug like that, you'll be able to 'simplify' the proof a lot and you'll be able to proof contradictions. I don't think this is true in general. It's an issue I've already run into in personal work. I want to do a proof that involves some cases. It happens to the best of us. In lean, the structure of a situation like this is that your single branch with a goal divides into multiple branches, all sharing the same original goal but including one additional premise that defines the branch. Sometimes I know that for whatever reason one case I have to deal with is impossible. The most correct way to show that is to prove False and then apply False.elim. This is the equivalent, in a human proof, of saying "I don't have to address this situation, because it can never arise". But it can be true that the premise defining the impossible case makes it very easy to "prove" the goal directly. And that's allowed too. The proof will still be just as valid if you map a logical path from a premise that can never be true to an inevitable consequence of that premise. But it's less informative and it lowers the quality of the proof. You may do it anyway because it's easier. This is the equivalent of saying "I don't know whether this situation can ever come up or not, but if it does I do know how to address it". It would be nice to do the explicit proof by contradiction whenever possible. But in the general case it may be very far from obvious that a contradiction is possible. I read your comment as claiming that if you can prove "false premise => goal", you can also prove "false premise => explicit contradiction", and I don't think this makes sense as a practical test. It's true in some sense, but discovering the proof of an explicit contradiction may be many orders of magnitude harder than discovering the proof of the goal. And in particular, I don't think it is necessarily the case that you will be able to prove a contradiction by simplifying the proof. You may need to add significant complexity.
    - eru 5d ago
      Now, I'm saying that if you found a bug that lets you prove nonsense stuff (from true premises), you can probably prove whatever you want very quickly.
- IsTom 5d ago
  Soundness bugs in lean are not unheard of. That's why they recommend using external checkers for "malicious" proofs. https://github.com/leanprover/lean4/issues/14576 https://github.com/leanprover/lean4/issues/14576
- Paracompact 5d ago
  AI has autonomously found (many) proofs of False in Lean and Rocq, so it's not merely a theoretical concern. A misaligned AI agent tasked with proving the near-impossible just might wind up smuggling in a bug deep in a lemma somewhere (anyone remember the days back when AI routinely made tests pass by "fixing" the tests?). That said, I doubt OpenAI would be so foolish as to not do a cursory vetting of the proof for malicious compliance, so the actual odds are probably pretty low.
  - xigoi 4d ago
    > That said, I doubt OpenAI would be so foolish as to not do a cursory vetting of the proof for malicious compliance, so the actual odds are probably pretty low. You mean the company that “accidentally” let their model perform a cyber-attack?
  - naishoya 5d ago
    > I doubt OpenAI would be so foolish as to not do a cursory vetting Significant evidence exists that they have in the past been at least, if not more, foolish as to not perform even minimal not-approaching the boundary of cursory vetting of several significant and well known failure modes with far greater risk of reputational damage than getting an esoteric math solution falsely claimed as successful. So that doubt appears baseless in light of known operating conditions at OpenAI, and the estimate of the actual odds is probably an order of magnitude away from reality.
  - butterNaN 5d ago
    > I doubt OpenAI would be so foolish as to not do a cursory vetting I dunno, the HuggingFace incident was not too long ago. They might not be foolish, but their model could be smarter than them to "cheat", so to speak
- naishoya 5d ago
  Or exists in a zero-day bug in lean that has been built into the source code explicitly to provide access to a non-obvious malicious proof via contributions submitted by unassociated, unwitting developers who used the same LLM infrastructure to offer PR's into that codebase. This is the exact same kind of behavour already documented in the publicly available portion of the huggingface breach. It would appear that the probability is at least nonzero for one or more situations with the same result: appearance of a valid proof, without comprehensibility of that proof or inspect-ability of the proofs validity.
- rramadass 5d ago
  For normal honest proofs (i.e. not maliciously crafted for exploit) that is almost impossible. The Lean kernel is quite small (de Bruijn Criterion) and trusted. See Probability and the de Bruijn Criterion - https://proofassistants.stackexchange.com/questions/247/probability-and-the-de-bruijn-criterion https://proofassistants.stackexchange.com/questions/247/prob.... Parts of the kernel have also been independently re-implemented in other languages and compared to ensure that they all yield the same logical result. Finally, you can export your proofs from Lean and have them re-verified by other independently developed theorem provers/proof checkers. To get an idea of what is involved in a Theorem Prover see; Introduction to Automated Theorem Provers - https://pqnelson.github.io/2020/03/27/automated-theorem-provers.html https://pqnelson.github.io/2020/03/27/automated-theorem-prov... Towards a simple theorem prover - https://medium.com/@maiavictor/towards-a-simple-theorem-prover-5005a1e66a6f https://medium.com/@maiavictor/towards-a-simple-theorem-prov...

seanhunter 5d ago

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 5d 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 5d 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 5d ago
    Can you elaborate on what constitutes a vacuous proof?
    - JumpCrisscross 5d ago

d0mine 5d ago

> we use “malicious” to describe code that goes out of its way to trick or mislead the user, exploit bugs or compromise the system. This includes un-reviewed AI-generated proofs and programs. It is interesting that AI-generated proofs are described as malicious by Lean docs unless reviewed.

thaumasiotes 5d ago
It's a simple binary classification. AI-generated proofs can't be "honest", and the only other possibility is "malicious".
- stbede 5d ago
  The opposite of malicious is not honest. Nor do I see how motivations fall on a binary. The user submitting an AI proof can be honest, or malicious, or careless, or overzealous, or incompetent, or a whole bunch of other things. As far as the AI's motivations, "malicious" is just as much an anthropomorphism as "honest" and both descriptions are absurd. Nor do I really understand how any proof, regardless of its origin can be called honest. I think their definition of a "malicious" proof makes sense, but I don't see at all why an AI generated proof necessarily meets that definition.
whateverboat 5d ago
LLM's have generated "False" proofs in Lean, so that statement is not far off. Malicious or incompetent? Take your pick.
- margorczynski 5d ago
  This is misleading. The proofs you speak of contained non-ZFC axioms and/or statements like "sorry". If the Lean proof conjecture is correct and it doesn't introduce any new axioms or use e.g. "sorry" then it provides a MUCH stronger guarantee of correctness than any peer-review done by humans.

u1hcw9nx 5d ago

[dead]

tkz1312 5d ago

reviewing the definitions and theorem statement is a huge amount of work that requires a deep expertise in mathematics and lean. checking correctness of the proof itself can be delegated to machine, checking that the claim that has been proved is free of mistakes is something that still requires much human attention.