4 ms·
I'm not totally sure what you mean. You can validate the proof using lean, which is what it's for--the whole magic of it is you don't have to just trust what A
by tmhn2 22d ago
I'm not totally sure what you mean. You can validate the proof using lean, which is what it's for--the whole magic of it is you don't have to just trust what AI says. That said, to your larger point, there are loopholes, and we'd certainly better be able to read the statement in lean, etc.
- evenhash 21d agoWhat I’m saying is that you can’t just trust what the AI says because it produces a Lean artifact. The statement of the theorem has to be correctly translated from English into Lean code. It’s like translating user requirements into code. The code could run without bugs but not do what the users want. The only way to know the AI did it correctly is to check. You can’t just take it at face value.
- tmhn2 20d agoYes, everyone is aware that the statement needs to be checked. No one has suggested otherwise. It goes without saying. The "magic" of lean is that (in principle, assuming lean is sound and the proof is verified) that is all you have to check by hand. That is a big deal.
- zahlman 20d agoJust because a proof is valid doesn't mean it proves the thing you want it to prove.
- tmhn2 20d agoOf course you must check the statement, that is obvious. The advantage (to put it mildly) is that you don't have to check the entire proof by hand.