@SidharthHariha1 @nytimes @NYTScience Aw man, that sucks. Hope you get some reasonable credit for this work.

@ShriramKMurthi @nytimes @NYTScience It’s certainly been a stressful few months!

We’ve got a preprint out describing this milestone, and once the project is finished, we’ll write a longer paper, crediting everyone involved (including collaborators from Math Inc).

https://arxiv.org/abs/2604.23468v3

@TaliaRinger "A proof [of the optimal solution of the sphere packing problem] evaded mathematicians until 1998."

But even that famously was too difficult for humans to referee, leading Thomas Hale, who proved the conjecture, to formalize it using Isabelle & HOL Light. https://en.wikipedia.org/wiki/Kepler_conjecture