AI Proof WatchKeep up with AI contributions

Log-concavity of codimension-three type-two pure O-sequences

A pure O-sequence records degree counts of monomials dividing a family of same-degree maximal monomials. Is every such sequence of codimension three and type two log-concave, so h(i−1)h(i+1)≤h(i)²?

Why it matters and what counts as progress

Why it matters: Log-concavity is stronger than the unimodality already known for this class.

What counts as progress: A proof at every interior degree for all codimension-three, type-two sequences, or an explicit pure O-sequence violating an inequality.

How the problem developed

  1. 17 Oct 2022 · Open case [1]

    Fabrizio Zanello Identified codimension three and type two as the remaining central case for log-concavity of pure O-sequences and proposed related conjectures.

  2. 21 May 2026 · Proof claim [2]

    Google DeepMind Agent (D) Reported a proof of Zanello’s conjecture establishing log-concavity for every pure O-sequence of codimension three and type two; the paper includes a Lean proof.

AI contribution

Advancing Mathematics Research with AI-Driven Formal Proof Search

George Tsoukalas, Anton Kovsharov, Sergey Shirobokov, Anja Surina, Moritz Firsching, Gergely Bérczi, Francisco J. R. Ruiz, Arun Suggala, Adam Zsolt Wagner, Eric Wieser, Lei Yu, Aja Huang, Miklós Z. Horváth, Andrew Ferraiuolo, Henryk Michalewski, Edward Lockhart, Codrut Grosu, Thomas Hubert, Matej Balog, Pushmeet Kohli, Swarat Chaudhuri

Every pure O-sequence of codimension three and type two is log-concave: h(i−1)h(i+1)≤h(i)^2 at every interior degree.

AI involvementAI-autonomous
ImportanceNotable
Technical verificationFormal (Lean 4)
Human understandingFull
Paper date:

Read the contribution and its assessment →

Sources

  1. Fabrizio Zanello, Log-concavity of level Hilbert functions and pure O-sequences
  2. DeepMind, Advancing Mathematics Research with AI-Driven Formal Proof Search
Website timeline

Publication dates and editorial changes.