math.AGMay 27, 2026

Real-rootedness of the Poincaré polynomials of M0,n\overline{\mathcal M}_{0,n}: an AI-assisted proof

Authors: Gergely BércziYoung-Hoon Kiem

Abstract

We prove real-rootedness for the Poincaré polynomial

Pn(t)=i=0n3dimH2i(M0,n;Q)tiP_n(t)=\sum_{i=0}^{n-3} \dim H^{2i}(\overline{\mathcal M}_{0,n};\mathbb{Q})t^i

of the Deligne--Mumford moduli space M0,n\overline{\mathcal M}_{0,n} of stable nn-pointed rational curves, proving a conjecture of Aluffi--Chen--Marcolli. The proof starts from the Keel--Manin--Getzler recurrence, but its main new idea is a bivariate deformation Fm(y,t)F_m(y,t) of the Poincaré polynomial. This deformation reveals a hidden interlacing structure not visible in the one-variable recurrence. For fixed t<0t<0, the zero set of FmF_m in the yy-direction is controlled by a Sturm--Rolle argument on the interval 0<y<1t0<y<1-t. The original polynomial is recovered on the slice y=1y=1, and the ordered crossings of the moving roots through this slice give both real-rootedness and strict interlacing. Consequently, the Betti numbers of M0,n\overline{\mathcal M}_{0,n} form an ultra-log-concave sequence. We further prove real-rootedness and ultra-log-concavity for the Poincaré polynomial of the Fulton--MacPherson space P1[n]\mathbb{P}^1[n] of nn ordered points in degenerations of the complex projective line. The proof for M0,n\overline{\mathcal M}_{0,n} was obtained through an iterative AI-assisted workflow with Co-Mathematician, an agentic frontier-model system developed by Google DeepMind. Our role was to formulate the problem, evaluate the proposed proof attempts, identify gaps and request corrections, compare the developing argument with the literature, and refine the presentation of the final proof. Our additional human contribution was to observe that a similar residual deformation strategy applies to the Fulton--MacPherson spaces P1[n]\mathbb P^1[n], yielding the corresponding real-rootedness theorem.

Explore similar work

May 24, 2026math.AG

Positivity in classical enumerative geometry: a case study in synchronized AI-assisted mathematics

We study the symmetric polynomial αAn,d(1+α1x1++αnxn)\prod_{α\in A_{n,d}}\bigl(1+α_1 x_1+\cdots+α_n x_n\bigr) where An,d:={αZ0n:α=d}A_{n,d}:=\{α\in\mathbb{Z}_{\ge 0}^n:|α|=d\}, which is the total Chern class of Symd(Cn)\mathrm{Sym}^d(\mathbb{C}^n), viewed as a torus representation whose Chern roots are the weights α1x1++αnxnα_1 x_1+\cdots+α_n x_n for αAn,dα\in A_{n,d}. Its homogeneous degree-kk part ck(n,d)c_k(n,d) is the kk-th Chern class of Symd(Cn)\mathrm{Sym}^d(\mathbb{C}^n). These Chern classes, together with their coefficients in various symmetric function bases, play a central role in enumerative geometry. Despite their simple definition, general closed formulas for their coefficients are subtle, and many structural properties of these classes have remained poorly understood. In this paper we prove several conjectures concerning their structure, establish explicit formulas, and study log-concavity properties for both the Chern classes and their KK-theoretic analogue. In rank two, passing to the Schur basis and expanding the Schur coefficients in the binomial basis of dd, we uncover a new binomial log-concavity phenomenon and prove refined positivity results. The paper demonstrates a novel methodology: we combine several AI systems with human mathematical insight in a coordinated workflow, deploying each tool according to its strengths in experimental discovery, conjecture formation, symbolic proof construction, and verification. To our knowledge, this is one of the first detailed case studies of orchestrating multiple AI tools to make substantial progress on a coherent mathematical research project.
Gergely Bérczi, László M. Fehér
Jun 4, 2026cs.SC

A Finite Certificate for the Positive n=9n=9 Vasc Inequality

We prove the positive-real n=9n=9 case of the Vasc cyclic inequality. The proof was obtained with human-guided assistance from the AI agent MechMath Agent Team: the human-readable part reduces the rational inequality to a homogeneous polynomial inequality, fixes a cyclic maximum, and parametrizes each sorted fixed-maximum cone by cumulative gaps; the finite part is a certificate covering all 8!=403208!=40320 sorted cones. MechMath Agent Team generated the certificate verification workflow through Python tool calls, including the case split, verification programs, and terminal classifications. The published certificate has 3681536815 coefficient leaves, 22362236 ordinary Polya multiplier leaves, and 12691269 AM-GM midpoint overlay leaves. Human authors audited the mathematical reductions and verification logic, and a separate artifact contains the certificate, an independent verifier, and a from-source rebuild route.
Dakai Guo, Ruichen Qiu, Yichuan Cao +1
Jun 24, 2026cs.LG

FactorLibrary: From Polynomials to Circuits via Recursive Subgoals

Finding minimal arithmetic circuits for polynomials over finite fields is a combinatorially hard problem central to algebraic complexity theory. We formulate it as a reinforcement learning problem in two directions, bottom-up and top-down. To address the challenge of a fast-growing combinatorial search space, we introduce FactorLibrary, which stores factorizable subexpressions that serve as reusable subgoals across training episodes. We trained a bottom-up agent with Gumbel-PPO-MCTS and two top-down agents with PPO+MCTS and SAC. The PPO+MCTS top-down agent exhibited the most stable performance, finding certified optimal circuits up to complexity 88 with a success rate of 91.8%91.8\%.
Rohan Pandey, Michael Ruofan Zeng, Weikun K. Zhang +5