3 ms·
What 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
by evenhash 20d ago
What 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 18d 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.