You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Sixteen independent Lean 4 packages, each self-contained on top of Mathlib.
One mathematical idea per package. Every unconditional theorem is fully proved;
conditional results carry explicit typed hypotheses (no package-local axioms).
v1.0.0 -- Hyperbolic and dispersive PDE
Package
Theorem
Status
ConservationLaws
Travelling step is a weak solution iff Rankine-Hugoniot holds (arbitrary flux)
Proved
BurgersBlowUp
No C^2 solution of Burgers reaches t = 1 for u_0(x) = -x
Proved
KdV
3c sech^2(sqrt(c)/2 x) is an exact soliton for all c > 0
Proved
v2.0.0 -- Riemann-von Mangoldt: zero counting and logarithmic residues
Package
Theorem
Status
DirichletEta
η(s) = (1-2^{1-s})ζ(s) (unconditional); non-vanishing of ζ on (0,1) conditional on RiemannZetaAlternatingLimitIdentity
Proved
ZetaZeroCounting
N(T) with multiplicities, safe heights, von Mangoldt main term
Proved
XiLogResidue
Logarithmic residue = multiplicity; dictionary with MeromorphicOn.divisor
Proved
XiLogDeriv
Expansion of Ξ'/Ξ; digamma identity for Γ_ℝ
Proved
v3.0.0 -- Meissel-Mertens constant and compensated convergence
Package
Theorem
Status
MertensPNT
Meissel-Mertens constant, compensated prime harmonic convergence, conditional PNT+ closure
Proved
v4.0.0 -- Argument principle, asymptotic synthesis, and discrete Abel-Chebyshev
Package
Theorem
Status
XiArgumentPrinciple
Contour/rectangle integral identity; conditional winding = count via typed ArgumentPrincipleBridge
Proved
XiAsymptoticFrontier
Conditional Riemann-von Mangoldt equivalence via typed AnalyticFrontier (7 fields)
Proved
DiscreteAbelChebyshev
Finite Abel summation; Chebyshev-to-prime error transfer via typed ChebyshevErrorSumBound
To our knowledge this is the first formalisation of weak solutions of
conservation laws, of Rankine-Hugoniot and Lax entropy conditions, of gradient
blow-up for a nonlinear PDE, of the KdV soliton, of the Riemann-von Mangoldt
zero-counting function, of the logarithmic-residue/multiplicity dictionary,
of the Meissel-Mertens constant with compensated convergence, of the
critical-box argument-principle contour chain for the entire Xi variant,
of the typed analytic-frontier synthesis for the asymptotic counting formula,
of the concrete Gell-Mann realisation of su(3) with certified structure constants,
of the SU(3) Wilson action positivity, of the kernel-certified LMFDB curve 5077a1,
and of the parity of nth-order prime-gap finite differences,
and of the smooth surgery-chain infrastructure for the conditional
4D Poincare conjecture,
in any major proof assistant.
Quick start
# Build and verify locally (Lean v4.31.0)
./M4TH.sh live # compile all .live.lean (16/16)
./M4TH.sh web <Pkg># compile .web.lean (v4.33.0-rc1, web env only)# Or work on a single package
./M4TH.sh build MertensPNT # build one package
./M4TH.sh live MertensPNT # compile .live.lean
./M4TH.sh web MertensPNT # compile .web.lean (v4.33.0-rc1)# Or directly per package (from monorepo root)
lake build MertensPNT
Axiom certificate
After a successful build, verify zero sorry and zero axiom:
# v1.0.0cd ConservationLaws &&echo'import ConservationLaws#print axioms ConservationLaw.hasShockIntegralReduction'| lake env lean --stdin &&cd ..
cd BurgersBlowUp &&echo'import BurgersBlowUp#print axioms Burgers.not_isRegularSolution_initialRamp'| lake env lean --stdin &&cd ..
cd KdV &&echo'import KdV#print axioms KdV.soliton_satisfies_kdv'| lake env lean --stdin &&cd ..
# v2.0.0cd DirichletEta &&echo'import DirichletEta#print axioms DirichletEta.zeta_real_open_interval_nonvanishing_from_eta'| lake env lean --stdin &&cd ..
cd ZetaZeroCounting &&echo'import ZetaZeroCounting#print axioms Riemann.zerosUpToIm_finite'| lake env lean --stdin &&cd ..
cd XiLogResidue &&echo'import XiLogResidue#print axioms RiemannLogResidue.entireXi_divisor_finset_eq_zerosUpToImFinset'| lake env lean --stdin &&cd ..
cd XiLogDeriv &&echo'import XiLogDeriv#print axioms RiemannLogDeriv.gammaRFactorLogDeriv_eq_neg_half_log_pi_add_half_digamma'| lake env lean --stdin &&cd ..
# v3.0.0cd MertensPNT &&echo'import MertensPNT#print axioms ErdosReciprocals.mertens_product_convergence'| lake env lean --stdin &&cd ..
# v4.0.0cd XiArgumentPrinciple &&echo'import XiArgumentPrinciple#print axioms RiemannArgumentPrinciple.entireXiContourIntegral_eq_rectangleIntegral'| lake env lean --stdin &&cd ..
cd XiArgumentPrinciple &&echo'import XiArgumentPrinciple#print axioms RiemannArgumentPrinciple.contour_winding_equals_count_of_safe'| lake env lean --stdin &&cd ..
cd XiAsymptoticFrontier &&echo'import XiAsymptoticFrontier#print axioms RiemannAsymptoticFrontier.riemann_von_mangoldt_from_contour_frontier'| lake env lean --stdin &&cd ..
cd DiscreteAbelChebyshev &&echo'import DiscreteAbelChebyshev#print axioms DiscreteAbelChebyshev.abel_summation'| lake env lean --stdin &&cd ..
cd DiscreteAbelChebyshev &&echo'import DiscreteAbelChebyshev#print axioms DiscreteAbelChebyshev.chebyshev_implies_prime_error'| lake env lean --stdin &&cd ..
# v5.0.0cd SU3Concrete &&echo'import SU3Concrete#print axioms Physics.YangMills.structureConstant_jacobi'| lake env lean --stdin &&cd ..
cd SU3Concrete &&echo'import SU3Concrete#print axioms Physics.YangMills.fundamentalCasimir_diagonal'| lake env lean --stdin &&cd ..
cd SU3Wilson &&echo'import SU3Wilson#print axioms Physics.YangMills.su3_trace_re_bound'| lake env lean --stdin &&cd ..
cd SU3Wilson &&echo'import SU3Wilson#print axioms Physics.YangMills.WilsonAction4D_nonneg'| lake env lean --stdin &&cd ..
cd CertifiedElliptic5077 &&echo'import CertifiedElliptic5077#print axioms CertifiedEC.shortDiscriminant_E5077'| lake env lean --stdin &&cd ..
cd CertifiedElliptic5077 &&echo'import CertifiedElliptic5077#print axioms CertifiedEC.P1_add_self'| lake env lean --stdin &&cd ..
cd PrimeGapsSophie &&echo'import PrimeGapsSophie#print axioms PrimeGapsSophie.sophie_germain_mod6_eq_5'| lake env lean --stdin &&cd ..
cd PrimeGapsSophie &&echo'import PrimeGapsSophie#print axioms PrimeGapsSophie.nthOrderGap_even_of_odd_primes'| lake env lean --stdin &&cd ..
Each must report only [propext, Classical.choice, Quot.sound].
Theorems
ConservationLaws -- scalar conservation laws
Theorem
Statement
hasShockIntegralReduction
Residual collapses exactly to R-H deficit along the interface
isWeakSolution_shockProfile_of_rankineHugoniot
Step is weak solution iff Rankine-Hugoniot holds
expansion_midpoint_is_weak_but_not_entropic
Expansion step violates the Lax entropy condition
BurgersBlowUp -- gradient blow-up
Theorem
Statement
constant_along_characteristic
u constant along x = x_0(1-t)
gradient_riccati_evolution
V'(t) = -V(t)^2 with V(0) = -1
gradient_eq_neg_one_div
V(t) = -1/(1-t) (exact Riccati solution)
not_isRegularSolution_initialRamp
No C^2 solution reaches t = 1
KdV -- exact soliton and conservation laws
Theorem
Statement
travellingWave_reduction
Travelling-wave ansatz reduces KdV to -c f' + f f' + f''' = 0
soliton_satisfies_kdv
3c sech^2(sqrt(c)/2 x) satisfies the soliton ODE for all c > 0
massRate_conserved
d/dt integral u = 0 for compactly supported smooth solutions
energyRate_conserved
d/dt integral u^2 = 0 for compactly supported smooth solutions
DirichletEta -- Dirichlet eta function
Theorem
Statement
eta_eq_zeta_of_re_gt_one
η(s) = (1-2^{1-s})ζ(s) for Re(s) > 1
zeta_real_open_interval_nonvanishing_from_eta
ζ(x) ≠ 0 for all x ∈ (0,1), conditional on RiemannZetaAlternatingLimitIdentity
ZetaZeroCounting -- Riemann-von Mangoldt N(T)
Theorem
Statement
zerosUpToIm_finite
Finite number of nontrivial zeros up to any finite height
exists_safe_height_above
Density of safe heights: every (T, T+ε] contains a height avoided by all zero ordinates
T_isLittleO_vonMangoldtMainTerm
T = o of the von Mangoldt main term (T/2π)(log(T/2π)-1)
Mathlib (pinned per package via lakefile.toml to fabf563a)
macOS / Linux / Windows
License
Software (.lean, .toml): Apache License 2.0 -- see LICENSE.
Documentation and paper (.md): CC-BY 4.0.
Citation
If you use this work in academic research, please cite:
@software{M4TH,
title = {M4TH: Formalised PDE and Analytic Number Theory in {Lean} 4},
author = {Izquierdo P{\'{e}}rez, Bezalel},
orcid = {0009-0001-5993-4057},
doi = {10.5281/zenodo.21646239},
year = {2026},
version = {v6.0.0},
url = {https://github.com/Alektronnik/M4TH}
}
