GPT-5.6 improved the bound on large prime gaps, and the proof is already formalized in Lean.

Number theorist Jared Duker Lichtman confirmed the result via r/singularity and his own posts, saving a factor of about log_3(n) over the 2018 Ford-Green-Konyagin-Maynard-Tao record, logged on erdosproblems.com/4 and formalized in Lean by Alexeev. The top comment makes the argument I'd make: the signal is the formalization, not the model. Prime gaps are a domain where a candidate proof is cheap to machine-check, so the model can search wide and let Lean grade. Expect the next records to fall in formalizable math specifically.