Surely with Lean this is just part and parcel of RLVR?
My best guess is “a huge number, and now the tail of the band between reliably solves and cannot solve is newsworthy,” but I don’t have particular knowledge of what they’re actually doing. It’s surprising to me that the Lean was apparently a post-hoc artifact from Astra, I would’ve expected all of these results to have been Lean spat out by a RLVR trace.
I doubt seemingly-curiosity-driven results like the Jacobian conjecture will remain typical for long.
Surely with Lean this is just part and parcel of RLVR?
My best guess is “a huge number, and now the tail of the band between reliably solves and cannot solve is newsworthy,” but I don’t have particular knowledge of what they’re actually doing. It’s surprising to me that the Lean was apparently a post-hoc artifact from Astra, I would’ve expected all of these results to have been Lean spat out by a RLVR trace.
I doubt seemingly-curiosity-driven results like the Jacobian conjecture will remain typical for long.