IMPA - O Instituto de Matemática Pura e Aplicada

Recent language models can do more than chat about mathematics: they can complete proofs, generate formal verifications, and occasionally settle open questions. I will examine what this means for research mathematics through two concrete case studies from my own work. The first is an old problem in classical invariant theory that sat unfinished in my notes for nearly a decade and was completed using Claude Code and Codex, with the key lemmas formally verified in Lean 4 via Harmonic's Aristotle prover. The second is even more striking: with minimal prompting, I got GPT-5.5 to prove the cubic analogue of a result of Laga and myself, showing that a positive proportion of hyperelliptic curves of large genus have no points over cubic number fields. In both cases, the AI contributed genuine mathematical ideas, and formal verification was essential to establishing that the resulting arguments were correct, catching errors in the process. I will use these examples to discuss where automated theorem proving and large language models are genuinely useful today, where they still fail, and why formalization is becoming more important, not less, as these systems grow more capable.

The Obata connection on a hypercomplex manifold is the unique torsion-free connection that preserves the hypercomplex structure. Up to taking the product with a torus, Joyce constructed left-invariant hypercomplex structures on compact semisimple Lie groups and certain related homogeneous spaces. Soldatenkov showed in 2011 that every Joyce hypercomplex structure on $SU(3)$ has Obata holonomy equal to the quaternionic general linear group and it was expected that the same should hold for all Joyce hypercomplex manifolds. For all such group manifolds except for $SU(2n+1)$, we will show that the holonomy group is strictly contained in the quaternionic general linear group. The case of $SU(2n+1)$ is more subtle, however for every $n > 1$, there still exist infinitely many Joyce hypercomplex structures with Obata holonomy strictly contained in the quaternionic general linear group and at least one with full holonomy on $SU(5)$. This talk is based on a joint work with Udhav Fowdar, Giovanni Gentili and Luigi Vezzoni.