★
Millennium & Smale Problems
Attacks on six open problems
Formal attempts at problems from the Clay Millennium Prize list and Smale's 1998 list. Each paper has a Lean-verified proof skeleton. These are ongoing research — the papers present proof strategies and verified components, not always closed proofs.
6 papers
Formal Verification
Working Paper
Lean
DOI
Flagship
Grade Decomposition and Gevrey Regularity for Navier-Stokes: A Machine-Checked Conditional Framework
We introduce a grade decomposition of the Gevrey energy balance for the incompressible Navier-Stokes equations. The physically correct model uses $\mathbb{C}$-valued Fourier coefficients with a factor of $i$ in the advection; the real-coefficient model trivializes all grade-3 terms.
Formal Verification
Working Paper
Lean
DOI
Flagship
Dimension-Independent Finiteness of Central Configurations for Positive Masses
We prove that for any $N \geq 3$ bodies with positive masses in $\mathbb{R}^d$ ($d \geq 2$), the number of central configurations modulo similarity is finite, resolving Smale's 6th Problem in **every spatial dimension $d \geq 2$ simultaneously**.
Mathematics
Draft
Lean
DOI
Flagship
The Riemann Hypothesis via Zeta Moment Hankel Positivity
We establish a conditional proof that the Riemann Hypothesis follows
from moment upper bounds weaker than the Lindelöf hypothesis.
Mathematics
Draft
DOI
The Euler Product Smoothness Theorem: Multiplicative Structure Forces Latent Existence
We prove that the distribution of values of random Euler products on the
critical line possesses a stable Latent — a finite rational approximation
with exponential convergence — and provide a **complete structural proof**
of the Euler Product Smoothn
Physics
Draft
DOI
Flagship
The Exact Latent Solution of the Gravitational Three-Body Problem
We argue that **every trajectory of the planar gravitational three-body problem** (excluding measure-zero triple collision) admits a finite Latent representation to arbitrary accuracy — an exact, implicit, constructive *encoding* in Fourier space — u
Physics
Working Paper
Lean
Turbulence Scaling Laws from the Grade Equation: Kolmogorov Spectrum and Intermittency from Analyticity
We derive the Kolmogorov energy spectrum $E(k) \sim \varepsilon^{2/3} k^{-5/3}$ and anomalous intermittency corrections to the structure function exponents $\zeta_p$ from the Grade Equation — a universal structural decomposition theorem for analytic dynamical systems. The derivation proceeds in three steps.