← All papers
Cubic Jordan algebras are not a series
math.RT
Jun 22, 2026 · v1
TL;DR
Certifies in Lean 4 the polynomial relations from a computer calculation showing the candidate series are finite point sets.
Abstract
The idea of the exceptional series is that the exceptional simple Lie algebras should form a series. Since all four simple Lie algebras in the fourth row of the Freudenthal magic square are exceptional it is natural to ask if the remaining rows form a series. A stronger version of this question is that, for the first two rows (corresponding to the real and complex numbers), there is a category defined by a presentation which is a reasonable candidate for the series. Our main results show that neither of these candidates is a series but each consists of a finite set of points. In each case the series is defined by a parameter and we show that the relations imply that this parameter satisfies a polynomial. These two results were obtained by a computer calculation. Our calculation is supported by a website for inspection, and the calculations are certified by Lean 4.
Problem
The exceptional simple Lie algebras form the fourth row of the Freudenthal magic square. The paper asks whether the remaining rows, or candidate categories defined by a presentation, also form a series.
Approach
A computer calculation derives the defining relations, which force the series parameter to satisfy a polynomial. The calculations are supported by an inspection website and certified by Lean 4.
Results
Neither candidate is a series; each consists of a finite set of points.