← All papers
First page of On the Quartic Invariant of Odd Degree Binary Forms

On the Quartic Invariant of Odd Degree Binary Forms

Ashvin Swaminathan

math.NT Mar 25, 2026 · v1
Key arithmetic lemmas about the quartic invariant of binary forms were formally verified in Lean 4 using Aristotle.
We determine the squarefree part of the scalar factor that arises when the quartic invariant of the generic binary form $F$ of odd degree $2n+1$ is expressed as the discriminant of the unique quadratic covariant $(F,F)_{2n}$. This squarefree part is exactly $p$ when $n+2$ is a power of an odd prime $p$, and $1$ otherwise. Equivalently, for each prime $p$: $v_2(S(n))$ is always even, and for odd $p$, $v_p(S(n))$ is odd if and only if $n+2$ is a power of $p$. This generalizes the classical identity $\operatorname{disc}(H(F))=-3\cdot\operatorname{disc}(F)$ for binary cubics, which dates back to the work of Cayley and Sylvester in the 1850s. The proof, which involves substantial explicit coefficient analysis and $p$-adic deformation arguments, was developed using an AI-assisted research workflow: the author's earlier partial attempts were completed through systematic collaboration with Claude Code (Anthropic) and Codex (OpenAI), and key arithmetic lemmas were formally verified in Lean~4 using Aristotle (Harmonic). We describe this workflow in detail as a case study in AI-assisted mathematical research. We also discuss representation-theoretic, geometric, and arithmetic interpretations of the quadratic covariant.

The classical identity disc(H(F)) = -3 * disc(F) for binary cubics, dating back to Cayley and Sylvester, relates the quartic invariant to the discriminant of the quadratic covariant. Generalizing this to odd-degree binary forms of arbitrary degree was open.

The author determines the squarefree part of the scalar factor when the quartic invariant of the generic binary form of odd degree 2n+1 is expressed as the discriminant of the unique quadratic covariant. The proof involves explicit coefficient analysis and p-adic deformation arguments. It was developed using an AI-assisted workflow: earlier partial attempts were completed through collaboration with Claude Code (Anthropic) and Codex (OpenAI), and key arithmetic lemmas were formally verified in Lean 4 using Aristotle (Harmonic).

The squarefree part is exactly p when n+2 is a power of an odd prime p, and 1 otherwise. Equivalently, for each prime p: v_2(S(n)) is always even, and for odd p, v_p(S(n)) is odd if and only if n+2 is a power of p.