Can’t wait to see the human verifying the results and then figure out that the AI model actually cheated and the results are not correct.
the proofs were verified in Lean, so unlikely.
Edit: at least ~600,000 lines
https://stanfordtechreview.com/articles/openai-buckmaster-na...