Proof Catalog

DOI-backed papers that have recorded Lean 4 verification artifacts. Verification scope varies by paper; open each entry for its stated assumptions, checked components, and remaining boundary.

31
Proof-Linked Papers
173
Tracked Claims
Lean 4
Proof Assistant
Stochastic Portfolio Theory, Machine-Checked: What Is Proven, What Is Sealed Against Mathlib, and What Stays a Modeling Assumption
Verified Formal Verification 18 theorems DOI
Where Does Mathematical Skill Live? A Controlled Biopsy of Transformer Mathematical Representations
Verified ml_general DOI
Certified Low-Rank Gaussian Processes via the Noise-Floor Rule
Verified machine_learning DOI
The Fenton Distribution: An Elementary Representation
Verified Quantitative Finance 9 theorems DOI
An Audited Contract Boundary for COS Caplet Pricing
Verified quantitative_finance DOI
Machine-Checked Scalar Foundations for SGD Analysis
Verified optimization and formal methods DOI
Conditional BSD Implications with Twelve Explicit Debt Assumptions
Verified number_theory DOI
From Design Points to Machine-Checked Parameter Regions: Reusable Certificate Templates for Engineering Models
Verified Formal Verification DOI
A Finite-Dimensional Bounded-Perturbation Certificate
Verified mathematics 12 theorems DOI
Conditional Bounds on AI Self-Improvement in an Antitone Threshold Model
Verified Formal Verification DOI
Formal Koide Structure: Mass Bounds, Generation Counting, and Neutrino Predictions from the Z_N Ansatz
Verified Formal Verification DOI
Toward the Riemann Hypothesis: A Superquadratic-Growth Framework for Zeta Moments and its Limits
Verified Mathematics 23 theorems DOI
Harvestability
Verified Formal Verification 22 theorems DOI
Resolving the Equity Premium Requires at Least Two Dimensions: A Machine-Checked Class No-Go and a Term-Structure Discriminator
Verified Formal Verification DOI
The Riemann Hypothesis via Fourier-Euler Product: A Short Conditional Reduction
Verified Mathematics 18 theorems DOI
The Projected-Generator Method for Path-Dependent Derivative Pricing
Verified Quantitative Finance 7 theorems DOI
Architectural Optimizations of the In-Context Gradient-Descent Mechanism
Verified machine_learning DOI
Capacity, Scaling, and Grokking from the In-Context Learning = Gradient Descent Mechanism
Verified machine_learning DOI
Training Dynamics and Inference Guarantees of the In-Context Gradient-Descent Mechanism
Verified machine_learning DOI
When In-Context Learning Implements Gradient Descent: A Learned Mechanism, Mechanically Verified and Empirically Tested
Verified machine_learning DOI
Explicit Flat Palm Weights for the Second Class Particle in a Three-State Attractive Interacting Particle System
Verified Formal Verification 3 theorems DOI
The Yang-Mills Mass Gap via Gauge Absorption and Perelman W-Entropy
Verified Formal Verification 5 theorems DOI
The Latent of Latents: Hierarchical Finite Representations of Knowledge Families
Verified Machine Learning 7 theorems DOI
Contaminated by Construction: Separating Simulation Noise from Model Risk in ES Backtests
Verified Quantitative Finance DOI
Deterministic Portfolio VaR Without Monte Carlo: The Eigen-COS Method
Verified Quantitative Finance 3 theorems DOI
Terminal Portfolio Value Distribution to Machine Precision
Verified Quantitative Finance 3 theorems DOI
What Is a Return? (Especially When Prices Can Be Negative)
Verified Quantitative Finance 5 theorems DOI
Grade Decomposition and Gevrey Regularity for Navier-Stokes: A Machine-Checked Conditional Framework
Verified Formal Verification 7 theorems DOI
Practical Padé Representations of the Gravitational Three-Body Problem
Verified Physics 1 theorems DOI
The Spectral Lognormal Distribution
Verified Quantitative Finance 19 theorems DOI
Fundamental Constants as Grade-Ratio Hypotheses
Verified Physics 11 theorems DOI