Papers With

← All papers
First page of A Polytopal Realization of Higher-Categorical Associahedra

A Polytopal Realization of Higher-Categorical Associahedra

Spencer Backman, Nathaniel Bottman, Daria Poliakova

math.CO Sep 21, 2026 · v1 math.AG math.MG math.SG
formalization combinatorics geometry ai-agents
Read PDF arXiv abstract
TL;DR
The authors used Anthropic's AI models to produce a Lean 4 formalization proving the barycentric velocity fan is polytopal for all categorical n-associahedra.
Abstract
We describe a polytopal realization of categorical $n$-associahedra. The normal fan of this polytopal realization is a modification of the authors' velocity fan and was found by OpenAI's Astra model.
Problem

Categorical n-associahedra, including 2-associahedra arising from functoriality of Fukaya categories, were given complete fan realizations via the velocity fan. That fan is not always polytopal: the 2-associahedron W_{1,1,1} is a counterexample. The goal is a fan realization that is always polytopal.

Approach

The velocity fan construction is modified to use barycentric terminal coordinates, giving the 'barycentric velocity fan'. Ray generators record changes in relative distances between lines and points during collisions. Explicit support function values are proposed to certify polytopality. The modification was found by OpenAI's Astra model, and a Lean 4 formalization of polytopality was produced with Anthropic's AI models.

Results

The barycentric velocity fan is announced to be polytopal for all categorical n-associahedra; per the authors, this is formalized in Lean 4, with a full written proof deferred to future work. For a single line it recovers the secondary fan of a polygon with vertices on a parabola, and it interpolates linearly with the original velocity fan.