> this is an opportunity for people to pick up where the model left off and run with it

Like people enjoy racing in front of a stopped train? As soon as they turn on the engine again, they will run you over. The questions that remain will be only the low value ones, not worth the effort to vacuum up.

So no, the smarter, hungrier people are not the ones that are going to swoop in. It will be the most desperate.

> Some output is going to be wrong or incomplete

This is a very human take on the situation. No, the Lean proof is not going to be wrong, and it will be incomplete only in the sense that OpenAI didn’t try to push the results further.