5 ms·

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

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 4d 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 4d 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 4d 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 4d 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 4d 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 3d 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 4d 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 4d 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 4d 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 4d 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...

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 4d 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 4d 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 4d 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 4d 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 4d 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 3d 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 4d 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 4d 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 4d 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 4d 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...