★
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.
5 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
DOI
Flagship
Toward Dimension-Independent Finiteness of Central Configurations for Positive Masses: A Scope-Audited Reduction with Named Open Bridges
A proposed route toward finiteness of central configurations for positive masses, with formalized components and explicit assumptions.
Mathematics
Draft
Lean
DOI
Flagship
Toward the Riemann Hypothesis: A Superquadratic-Growth Framework for Zeta Moments and its Limits
We present an algebraic framework relating the growth of the zeta
moments to Hankel-determinant structure, together with an honest
account of where the framework does and does not reach the Riemann
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
Toward an Exact Latent Encoding of the Gravitational Three-Body Problem
A proposed finite Latent encoding for gravitational three-body trajectories, with convergence and formalization status separated from the main claim.