|
|
|
|
|
|
by andor
1 day 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. |
|
|
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.