Hacker News Reader

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.

View on HN

> 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.

Reply on news.ycombinator.com