AI-Assisted Discovery of a Polynomial Lyapunov Potential for the Antiferromagnetic Potts Model

Progress in AI for mathematics is largely measured on benchmarks and competition problems, leaving a gap with the questions working mathematicians actually care about. We argue for a different entry point: problems whose key idea is simple once seen, yet whose search and verification are tedious. As a case study from a working mathematician's perspective, we revisit an already-resolved problem and find a genuinely new proof of it: uniqueness of the Gibbs measure for the three-state antiferromagnetic Potts model on the infinite binary tree at every positive temperature. Where prior proofs control the tree recursion through two-step compositions and delicate computer-assisted estimates, we construct a new one-step polynomial Lyapunov potential on the simplex that reduces the whole problem to a single finite-dimensional inequality---which we then discharge by harnessing AI's strength in symbolic computation and exact verification, via a Bernstein-basis certificate. Beyond the proof itself, we report on the agentic workflow that led to it: we tried several AI-driven paths to this problem---autonomous proof search, adversarial potential discovery, and formal-prover attempts---and summarize what worked and what did not, offering a few concrete lessons for using current agents in this kind of search-and-verify mathematics.