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. 573 papers, 347 Lean-verified, 6,071 theorems.

Start Here See the Problems Explore the Graph

573

Papers

347

Lean-Verified

DOIs

6,071

Theorems

Domains

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**.

18,003 words 1 claims

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.

80,076 words 35 claims

Flagship Quantitative Finance Lean

The Fenton Distribution Solved

The moment-based Latent representation of correlated lognormal sums (Nagy, 2026, *The Exact Latent Distribution of Correlated Lognormal Sums*) relies on scaled moments $c_k = m_k/k!$ that grow as $e^{\sigma_{\max}^2 k^2/2}$.

14,277 words 10 claims

Flagship meta-methodology Lean

The Operational Curry–Howard: Proof Discovery as Navigated Software Architecture

We propose a framework that unifies two perspectives on formal proof construction: **proof as pathfinding** in a type-theoretic state space and **proof as programming** via the Curry–Howard correspondence.

37,516 words 26 claims

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.

19,040 words 27 claims

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

11,407 words 3 claims

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.

9,471 words 7 claims

Flagship Machine Learning Lean

Neural Scaling Laws Formalized: Why Chinchilla Works (A Machine-Verified Derivation)

Neural scaling laws — the empirical observation that test loss decreases as a power law in compute budget — are the foundation of modern AI training strategy. Every major laboratory trains billion-dollar models by extrapolating scaling curves, yet *why* these power laws hold remains unexplained.

8,417 words 20 claims

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

3 papers →

★

Millennium & Smale Problems

Attacks on six open problems

6 papers →

✓

Machine-Verified Proofs

Papers with Lean 4 formal verification

20 papers →

▲

AI: Safety, Scaling, Interpretability

Machine learning results with formal guarantees

8 papers →

Quantitative Finance

Exact pricing, risk, and distributions

8 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%

2 papers →

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%

1 paper →

▲

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%

3 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