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 →