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.