Machine-proved results for open mathematical problems.
Attacking Navier–Stokes, Riemann, Collatz, and more — with Lean 4 machine-verified proofs and a unified algebraic framework. 26 papers, 16 Lean-verified, 272 theorems.
Flagship Papers
All collections →The strongest results in the corpus. If you read only a few papers, read these. They are the trust-layer entry points for every other page on the site.
Flagship
Formal Verification
Lean
DOI
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**.
Flagship
Core Theory
Lean
DOI
The Latent: Finite Sufficient Representations of Smooth Systems
We define the **Latent** of a smooth system as the basis-free element of a graded Hilbert tensor algebra that completely characterizes the system's distributional, dynamic, and functional properties.
Flagship
Mathematics
Lean
DOI
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.
Flagship
Physics
DOI
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
Flagship
Formal Verification
Lean
DOI
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.
Collections
All 10 collections →Curated reading lists — each collection is 3 to 20 papers organized around a theme, problem, or methodology. Start here instead of the raw archive.
◆
Start with the Latent
Three papers that introduce the core framework
2 papers →
★
Millennium & Smale Problems
Attacks on six open problems
5 papers →
✓
Machine-Verified Proofs
Papers with Lean 4 formal verification
14 papers →
▲
AI: Safety, Scaling, Interpretability
Machine learning results with formal guarantees
0 papers →
$
Quantitative Finance
Exact pricing, risk, and distributions
3 papers →
π
Number Theory & the Riemann Hypothesis
Paths toward RH and related prime distribution results
4 papers →
Open Problems
All problems →The research program targets specific open problems in mathematics and physics — not general-purpose theorem-proving. Each entry links to the papers that make direct contributions.
∇
Navier–Stokes Global Regularity
Clay Millennium Problem
Do smooth initial conditions always give smooth global solutions to the 3D incompressible Navier–Stokes equations?
Conditional framework verified
60%
1 paper →
ζ
Riemann Hypothesis
Clay Millennium Problem
Do all non-trivial zeros of the Riemann zeta function have real part exactly 1/2?
Conditional proof via two routes
55%
4 papers →
◯
The Three-Body Problem
Smale's 1998 list, Problem 5
Is there a closed-form, non-perturbative description of gravitational three-body motion in the general case?
Exact solution paper complete
75%
1 paper →
✦
Central Configurations Finiteness
Smale's 1998 list, Problem 6
For each n ≥ 4, are there only finitely many central configurations of n point masses under Newtonian gravity?
Lean-verified proof skeleton
80%
1 paper →
≋
Turbulence Scaling
Kolmogorov's 5/3 law and beyond
Can the empirically observed scaling exponents of high-Reynolds-number turbulence be derived from first principles?
Framework paper drafted
40%
0 papers →
▲
Neural Scaling Laws
Why do large language models work?
Why does model performance follow power laws in compute, data, and parameters? And when should we expect it to break?
Machine-verified derivation
85%
0 papers →
From the Blog
All posts →Research diary — the intuitions behind the proofs, open questions, and what I'm working on. Like a seminar talk, but you can read it at your own pace.
2026-04-22
Why random matrix theory keeps appearing in Riemann zeros
Montgomery's 1973 observation — that the pair correlation of Riemann zeros matches the GUE ensemble of random matrix the…
number-theory
riemann-hypothesis
random-matrices
2026-04-20
What does Lean 4 actually check in a number theory proof?
People hear "machine-verified proof of the Riemann Hypothesis" and imagine the computer checking every $\varepsilon$-$\d…
lean4
formal-verification
methodology
2026-04-18
One algebra, six open problems
When I tell people the same algebraic framework applies to Navier–Stokes, the Fenton distribution, and neural scaling la…
latent-framework
cross-domain
tensor-algebra
Program-Level Artefacts
◆
The Latent Framework
Unifying algebraic structure
2 papers reuse the same core algebra across finance, physics, ML.
Explore the framework →
✓
Proof Catalog
Machine-verified theorems
0 proof records containing 0 Lean 4 theorems.
Browse the catalog →
◷
Recent Updates
What's new in the corpus
Latest additions and revisions to the paper set. RSS available.
See the timeline →