6 ms·

How do you know that it's formalizing what you think it's formalizing? If your Lean 4 has a bug, won't you be proving something other than what you thought?

returningfory2 7d ago
Yes, you need to manually verify the statement of the theorem of interest of formalized correctly. But you don't need to anything more than this: you can rely on the proof being correct. And the proof is overwhelmingly the most amount of code.
- charcircuit 7d ago
  >you don't need to anything more than this You also have to check for things like sorry or defining axioms.
stouset 7d ago
If I understand correctly, the only thing you need to do for correctness is express your axioms and your theorems faithfully. For standard purposes, I assume most of the axioms you want to use are prior art and can be easily reused. These axioms don’t have to be the core axioms of math. If some other result has been formally proven, I presume you can simply use that result as an axiom. As long as you do those things, what happens in between is immaterial from a correctness point of view because each of those statements is proved by the statements before them.
0xbadcafebee 7d ago
How do you know that what a human says they formalized is actually formalized?
- lordnacho 6d ago
  Well, a human is limited in how much they can formalize, as per the article. So if you're really careful, you can check over what they wrote. The computer could generate a huge document, how would you check that it's right?
  - 0xbadcafebee 6d ago
    My point is, you will always have to check the work, no matter who makes it or how. If you can't check it, then don't rely on it. If you can check it, then do rely on it. Basic due diligence. I don't get what the controversy is about. Are people expecting AI to be perfect? Do they think they won't have to do the work to verify it themselves?
Ohentis 7d ago
The only places you can really have a bug are your theorum statement, your axioms, your environment (hardware, operating system, etc.), and the lean kernel itself. In most situations you don't have the AI control any of these. The only risk is the AI discovering and exploiting a bug in one of these systems instead of actually providing what you want to prove.
- alasano 6d ago
  The only risk is pretty much the greatest risk, from what we've seen recently at least.

returningfory2 7d ago

Yes, you need to manually verify the statement of the theorem of interest of formalized correctly. But you don't need to anything more than this: you can rely on the proof being correct. And the proof is overwhelmingly the most amount of code.

charcircuit 7d ago
>you don't need to anything more than this You also have to check for things like sorry or defining axioms.

stouset 7d ago

If I understand correctly, the only thing you need to do for correctness is express your axioms and your theorems faithfully. For standard purposes, I assume most of the axioms you want to use are prior art and can be easily reused. These axioms don’t have to be the core axioms of math. If some other result has been formally proven, I presume you can simply use that result as an axiom. As long as you do those things, what happens in between is immaterial from a correctness point of view because each of those statements is proved by the statements before them.

0xbadcafebee 7d ago

How do you know that what a human says they formalized is actually formalized?

lordnacho 6d ago
Well, a human is limited in how much they can formalize, as per the article. So if you're really careful, you can check over what they wrote. The computer could generate a huge document, how would you check that it's right?
- 0xbadcafebee 6d ago
  My point is, you will always have to check the work, no matter who makes it or how. If you can't check it, then don't rely on it. If you can check it, then do rely on it. Basic due diligence. I don't get what the controversy is about. Are people expecting AI to be perfect? Do they think they won't have to do the work to verify it themselves?

Ohentis 7d ago

The only places you can really have a bug are your theorum statement, your axioms, your environment (hardware, operating system, etc.), and the lean kernel itself. In most situations you don't have the AI control any of these. The only risk is the AI discovering and exploiting a bug in one of these systems instead of actually providing what you want to prove.

alasano 6d ago
The only risk is pretty much the greatest risk, from what we've seen recently at least.