AI Proof WatchKeep up with AI contributions

An Efficient Triangulation of ℝP⁵

Dan Guyer, Stefan Steinerberger, Yirong Yang

A centrally symmetric simplicial six-dimensional polytope with 48 vertices has an antipodal boundary quotient that triangulates real projective five-space on 24 vertices.

Sources for this record

What was already known

Lutz already had a combinatorial 24-vertex triangulation of RP⁵. A general lower bound is 22 vertices; a polytopal antipodal realization at 24 was not known.

AI involvement AI-centered

The humans chose the geometric objective and ran AlphaEvolve as black-box optimization. It found a 48-point candidate. Their subsequent L1 rotation and sparsity search exposed a structured family and the final rational coordinates. The model-discovered seed was central to this retained construction, while the structure and proof are human work.

AlphaEvolve found the 48-point candidate from which the authors recovered the final construction; the model did not supply the final sparse coordinates or proof.

Importance Notable

Provides a new geometric realization at the known 24-vertex count.

Limitations

This is not the first 24-vertex triangulation and does not establish vertex minimality. AlphaEvolve found a candidate; Guyer, Steinerberger and Yang recovered the final rational coordinates and report exact SageMath checks.

Technical verification Formal (SageMath 10.3 exact polytope computation)

The paper reports exact SageMath checks that the displayed rational polytope is simplicial and its antipodal vertices have disjoint neighbor sets, the finite conditions yielding the stated quotient triangulation. The linked notebook covers the polytopes and Lutz comparison. This review did not run it.

Formal checking

Facet and 1-skeleton computation on rational coordinates, including simpliciality and antipodal-neighborhood tests

Checker
SageMath 10.3 notebook reported by Guyer, Steinerberger and Yang
Scope
The explicit 48-vertex rational 6-polytope is simplicial and satisfies the antipodal quotient condition for a 24-vertex RP^5 triangulation
Basis
Reported by the linked checker
Evidence source

Checking a formal statement does not establish that it matches the original problem.

Human understanding Full

The authors explain how the candidate led through L1 sparsification to six overlapping cube supports, give rational coordinates and analyze the quotient graph.

Correction and publication history