Every time I’ve organized my thoughts sufficiently to finally write a proper blog post about the impact of AI on mathematical research, something massive happens which causes me to delay. I was preparing to wrote a post last week when I heard about the formalization of Fermat’s Last Theorem in Lean. And I was preparing to write a post this week when the news broke about an AI-assisted solution of the Millennium Prize Navier-Stoker problem. Rather than delay again (what will the big breakthrough be next week?), let me just record some thoughts quickly while I have a few moments to spare before heading to bed. This will not be as organized, or as carefully thought out, as I had hoped, but the speed at which the mathematical landscape is changing does not seem to allow for a leisurely collection of thoughts. I imagine I will come back to many of these topics in the future.
Continue readingCategory Archives: A.I.
The geometry of snowflaked Ptolemaic metric spaces
My coauthors June Huh, Mario Kummer, Oliver Lorscheid, and I just posted a paper called Lorentzian polynomials and matroids over triangular hyperfields, Part 2: Analytic aspects on the arXiv preprint server. This is the first paper of mine to contain a substantial result proved by AI, and also the first to contain a proof formally verified in Lean. So I thought I would take this opportunity to tell a bit of the backstory.
Although our paper is motivated by the general theory of Lorentzian polynomials and matroids with coefficients, which are a bit daunting to explain in a short post, the parts in which AI played a decisive role can be explained in a completely elementary way. I will first state some of our main results, as well as our main open conjecture, in terms of basic linear algebra. Then I will discuss how AI—primarily Chat GPT-5.5—was able to prove a theorem that had previously eluded us. Continue reading
