Machine-Verified Proofs — Collections

Mathematics Working Paper Lean

M1 — Mesoscopic-decay extremal function (working file)

87,634 words 5 claims

Core Theory Draft Lean DOI Flagship

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

Formal Verification Draft Lean

The PDE Tensor Algebra: Structural Decomposition and Exact Recombination of Differential Equations

We introduce the **PDE Tensor Algebra**, a framework that represents any PDE system as a triple $(D, C, P)$ of tensors encoding dissipation, nonlinear coupling, and geometric constraints. The decomposition converts qualitative PDE questions — existence, uniqueness, regularity, stability — into computable algebraic conditions on the tensors.

67,878 words 24 claims

Formal Verification Draft Lean

Critical Exponents for Three-Dimensional Percolation: A Crossover Approach via Long-Range Renormalization

37,738 words 2 claims

meta-methodology Draft Lean Flagship

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

Physics Draft Lean

Existence and Mass Gap for Yang-Mills Theory on R^4

We prove that for any compact simple gauge group $G$, quantum Yang-Mills theory on $\mathbb{R}^4$ exists as a Wightman quantum field theory and has a mass gap $\Delta > 0$, solving the Clay Mathematics Institute Millennium Problem of Jaffe-Witten in

25,669 words 1 claims

number_theory Draft Lean

ε-Removal for Moments of the Riemann Zeta Function via Cumulant Generating Function Analysis, Subject to Grade-2 Dominance

Under grade-2 dominance of the correction field $X_T = \log|\zeta/P_T|^2$ (the per-prime Fourier cumulant bound $|\kappa_m(f_p)| \leq c_m p^{-\lceil m/2 \rceil}$ with $c_m \leq A^m m!$ giving a positive CGF-tail convergence radius $r_\star \geq 1/A$;

22,090 words 8 claims

mathematics Draft Lean

Proof Circuits

Many of the deepest theorems in mathematics were not proved within a single domain but by transferring the problem through a sequence of domains, applying tools native to each, and returning.

21,446 words 1 claims

Formal Verification Draft Lean DOI

The Yang-Mills Mass Gap via Gauge Absorption and Perelman W-Entropy

**Theorem A (Main result, conditional).** Conditional on the 20 named Tier A–D hypotheses of §7.1 — in particular the three Tier-D perturbative-QFT inputs (`tomboulis_formula`, `b_zero_from_feynman`, `beta_1_rge_def`) — we establish that Yang-Mills t

20,020 words 5 claims

Formal Verification Working Paper Lean

A Machine-Checked Reduced Transport Law for Stochastic-Field-Line Confinement

We present a machine-checked reduced transport law for ion-scale turbulent confinement in tokamak plasmas.

19,276 words 14 claims

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.

19,040 words 27 claims

number_theory Draft Lean

A Unified Resonance Framework for the Riemann Hypothesis

We introduce a resonance algebra framework that unifies four classical approaches to the Riemann Hypothesis into a single structure. Each non-trivial zero $\rho_n = \sigma_n + i\gamma_n$ of $\zeta(s)$ is modeled as a resonance mode with damping rate $\sigma_n$ and frequency $\gamma_n$.

18,863 words 3 claims

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

18,003 words 1 claims

number_theory Draft Lean

A Lean 4 Formalization of the Birch and Swinnerton-Dyer Conjecture and Its Surrounding Theory

The Birch and Swinnerton-Dyer conjecture predicts that for an elliptic curve $E/\mathbb{Q}$ the Mordell-Weil rank equals the order of vanishing of the Hasse-Weil $L$-function at $s = 1$, and that the leading Taylor coefficient is expressed by an expl

16,260 words

mathematics Draft Lean

The Convolution–Correlation Duality

We identify a structural dichotomy — the *convolution–correlation duality* — that governs whether problems involving oscillatory spectral expansions are tractable. The principle is this: when a quantity is formed by convolving independent components, each independent integration contributes a damping factor to the spectral coefficients.

15,319 words 5 claims

Quantitative Finance Draft Lean Flagship

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

quantitative_finance Draft Lean

The ATM Skew Power Law: A Machine-Verified Derivation from the rBergomi Model

We derive the ATM implied volatility skew power law $\psi(T) \sim C \cdot T^{H-1/2}$ from the rough Bergomi (rBergomi) model through a machine-verified chain of 125 theorems.

14,265 words 62 claims

number_theory Draft Lean

The Goldbach Conjecture as a Latent Positivity Theorem: Twenty-Five Paths, the Convergence Theorem, and the Five-Layer Strategy

We develop a conditional proof program for the Goldbach conjecture through the generating function $G(z) = P(z)^2$, where $P(z) = \sum_{p \text{ prime}} z^p$.

13,736 words 56 claims

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.

12,483 words 3 claims

Quantitative Finance Working Paper Lean DOI

Contaminated by Construction: Separating Simulation Noise from Model Risk in ES Backtests

Expected Shortfall backtesting under Basel III/IV suffers from an unmeasured structural weakness: Monte Carlo estimation of ES injects computational noise into the Acerbi-Székely (2014) test statistic, but the magnitude of this contamination has not

12,334 words