About the atlas

The atlas collects sequences of polynomials $P 0, P 1, \dots$ with integer coefficients for which every polynomial is proved to have only real roots, for every $n$ . The proofs are found automatically by polytool.

Each sequence is given by a recurrence. Its page shows the first rows, the proved properties (an interval containing all roots, interlacing of consecutive rows, sign of the coefficients) and text ready to submit to the OEIS.
Each property has a proof: either a direct theorem check of the recurrence, or a step that derives it from other sequences in the atlas (for instance an image under a map that preserves real-rootedness). Every step carries a certificate that polytool replays, and cites the theorem it uses.
OEIS matches compare the published terms with the rows, row by row. A match is agreement on finitely many terms, not a proof that the two sequences are equal.
The chips nonnegative coefficients (nonn) and only rational roots (rr_by_factors: every row is a product of linear factors over ℚ), and likewise palindromic and γ-positive, are observed on the stored rows, not proved.

For the proof methods, see the list of operations. Everything on these pages is also available through the JSON API.