Comment by andor
9 hours ago
The LLM does not prove anything (it cannot reason). It generates Lean code, and conveniently, in Lean, the code is also the proof. It’s not merely a model of the stated system, it is the system.
You still need to verify that the generated code is what you asked for, though.
> The LLM does not prove anything (it cannot reason).
What is that supposed to mean?
> It generates Lean code, and conveniently, in Lean, the code is also the proof. It’s not merely a model of the stated system, it is the system.
Yes, and that's great. (Though, of course, the computer doesn't execute lean directly, it gets translated first.)
> You still need to verify that the generated code is what you asked for, though.
Yes, but you only need to read the theorems, not the proofs nor code.