Hacker News Reader

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

View on HN

It's less useful, because humans make fewer mistakes and take longer to turn their thoughts into Lean. I think most mathematicians have a higher success rate thinking about the problem informally, poking at it themselves, then formalizing it iteratively to make it more watertight as they gain confidence in the idea.

> humans make fewer mistakes

Is this empirically measurable?

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.

But a human being using LLMs will be much more creative than just LLMs alone right? Or does the human reduce the creativity in this system in your opinion?

> But a human being using LLMs will be much more creative than just LLMs alone right?

I believe so. But the question I was responding to was whether humans working with Lean would be have been more creative.

> Or does the human reduce the creativity in this system in your opinion?

Yes. Humans are slow.

Reply on news.ycombinator.com