Complex systems research, made checkable.
Thalens is an independent research hub across AI, finance, physics, and mathematics. The work uses papers, code, empirical tests, formal verification, and explicit assumptions to make research claims concrete.
Flagship Papers
All collections →Curated entry points into the corpus. If you read only a few papers, read these first; each one carries its own status, assumptions, and verification boundary.
Flagship
Formal Verification
Lean
DOI
Dimension-Independent Finiteness of Central Configurations for Positive Masses
A proposed route toward finiteness of central configurations for positive masses, with formalized components and explicit assumptions.
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
A proposed finite Latent encoding for gravitational three-body trajectories, with convergence and formalization status separated from the main claim.
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
16 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 studies specific open problems in mathematics and physics through approaches, reductions, and partial structures. Each entry links to papers that state their assumptions and remaining gaps.
∇
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 reduction 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?
Approach paper published
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?
Conditional 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
Formal artifacts and trust boundaries
0 proof records containing 0 theorem statements and checks, with assumptions surfaced where applicable.
Browse the catalog →
◷
Recent Updates
What's new in the corpus
Latest additions and revisions to the paper set. RSS available.
See the timeline →