I really love this quote by @TaliaRinger. I think there’s potential for a beautiful complementarity between the roles of humans and AI models/companies - but we need to realise that potential!

(This quote is NOT about claims made during this specific incident. Read the article!)

The linked article is a nuanced take on the social side of AI math formulation.

Talia's quote crystallized a bunch of things I've noticed about AI programming: “They weren’t going to subsume the work I was doing, but they were going to claim to subsume the work I was doing,”

We live in interesting times, and now a little episode from my life lives in the Times as well… @nytimes @NYTScience

https://www.nytimes.com/2026/06/08/science/ai-scoop-young-mathematicians.html

@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

Neat to see this article come out as I'm navigating fears of this in the Agda community

https://www.nytimes.com/2026/06/08/science/ai-scoop-young-mathematicians.html?unlocked_article_code=1.olA.dJte.wZXzslO706sU&smid=url-share

@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