> Initially, the rumors about these OpenAI results had it that there were solutions to 400 problems, and now the rumors are that further dumps are arriving soon.
That is mental if true. Though if once again most of them will lack a Lean proof, bit hard to feel confident about their correctness. They might trust their model, but given the community impressions on manuscript prose quality, I have a hard time imagining they are any better than its coding output, where closed loop verification continues to be essential. OpenAI might have great trust in their internal model, but this seems like a needlessly hazardous way test that trust out. The optics of those retracted papers from a few days ago were bad enough already.
I have separately heard of efforts regarding Lean proof optimization. Since it's all self machine checkable, might be valuable to do before a release like this too. I'd imagine a shorter Lean proof means a shorter manuscript too.
That is mental if true. Though if once again most of them will lack a Lean proof, bit hard to feel confident about their correctness. They might trust their model, but given the community impressions on manuscript prose quality, I have a hard time imagining they are any better than its coding output, where closed loop verification continues to be essential. OpenAI might have great trust in their internal model, but this seems like a needlessly hazardous way test that trust out. The optics of those retracted papers from a few days ago were bad enough already.
I have separately heard of efforts regarding Lean proof optimization. Since it's all self machine checkable, might be valuable to do before a release like this too. I'd imagine a shorter Lean proof means a shorter manuscript too.