Ternary polynomial relations and periods of cusp forms
Vasily Ilin, Ken Ono
math.NT
Oct 13, 2026 · v1
TL;DR
The main theorems (1.1, 1.2) and essential argument are formalized in Lean 4 with Mathlib by AxiomProver, with no admissions and only standard axioms.
Abstract
Bachmann and van Ittersum conjectured that every polynomial $f\in\mathbb{Q}[x,y,z]$ satisfying $$ f(x,y,z)=f(y,z,x),\qquad f(x,y,z)+f(-y,x-y,z)+f(y-x,-x,z)=0 $$ is a sum of polynomials in two variables. We prove this conjecture over every field of characteristic zero and determine all homogeneous solutions. Moreover, restriction to $z=0$ identifies the degree $n$ solution space with the space of binary period polynomials of degree $n$ normalized to vanish on both coordinate axes. The solution corresponding to such a polynomial $q$ is $$ f(x,y,z)=q(x,y)+q(y,z)+q(z,x). $$ There are no nonzero homogeneous solutions of odd degree. For even degrees $n$, the symmetric and alternating solution spaces are each isomorphic over $\mathbb{C}$ to the space of weight $n+2$ cusp forms on $SL_2(\mathbb{Z})$. The proof connects the polynomial relations with the cohomology of arithmetic groups through the rational Tits building for $GL_3$. Cusp forms enter both the description of the solutions and the proof that there are no others. The main theorems and the essential argument are formalized unconditionally in Lean 4 by AxiomProver.
Problem
Bachmann and van Ittersum conjectured that every rational polynomial in three variables satisfying a cyclic symmetry and a three-term period relation is a sum of two-variable polynomials. The structure of all homogeneous solutions was also open.
Approach
The polynomial relations are connected to the cohomology of arithmetic groups through the rational Tits building for GL_3. Solutions are identified with polynomial-valued functionals on incidence graphs, and extension obstructions are removed using Hecke operators and L-value nonvanishing. Symmetric and alternating cases are treated separately, with a mod four argument for odd degree. The main theorems and the essential argument were formalized in Lean 4.35.0 with Mathlib, written in collaboration with the AI system AxiomProver.
Results
The conjecture holds over every field of characteristic zero, and there are no nonzero odd-degree homogeneous solutions. In each even degree n, the solutions are q(x,y)+q(y,z)+q(z,x) for normalized binary period polynomials q. Over C, the symmetric and alternating solution spaces are each isomorphic to the space of weight n+2 cusp forms on SL_2(Z). The Lean development is free of admissions.
