alt Hacker NewsMake a trivial adjustment to your final proposition and it would still hold, no?
> Humans have quite a bit of creativity but make a lot of mistakes. The Lean typecheck never makes a mistake but has no creativity. Get them to work together in an iterative loop and you get what we have now.
The speed matters massively. Also it seems that LLMs are... getting to be quite creative.
The point is that the there has to be an idea to try to check. Lean does not give you that.