$m$ is a moment sequence iff every real Hankel matrix $\Delta_n$ is positive semidefinite

Let $m=(m_n)_{n\ge0}$ be a real sequence. Then $m$ is the moment sequence of some positive Borel measure on $\mathbb R$ if and only if, for every $n\ge0$, the real Hankel matrix

is positive semidefinite.

This is the real-coefficient form of Hamburger's characterization: positive semidefiniteness of the Hankel matrices is necessary for $m$ to be a moment sequence and sufficient for the existence of a positive measure.

Formalization Note Positive semidefiniteness is Mathlib's Matrix.PosSemidef (symmetric, with $x^{\mathsf T}\Delta_nx\ge0$ for all $x\in\mathbb R^{n+1}$).