Lean 4 formalization and certificate checking for total coloring and auxiliary rainbow edge-coloring reductions
Kernel-checked random-matrix and analytic foundations in Lean 4: Airy and Tracy-Widom distributions, Fredholm series, Marchenko-Pastur, Stieltjes transforms
Neumann cosine series on [0,L] and the discrete Neumann Laplacian in Lean 4 and Mathlib
Scalar pitchfork bifurcation with jet-bounded remainder, and the topology of global branches, in Lean 4 and Mathlib
Consumer pilot of scottnarmstrong/MarkovProcess: two Brownian-motion theorems, with lean-pkg receipts
Lean 4 formalization of the finite algebraic core (Ward, closure and energy identities) of a 2D Anderson-model paper; the localization theorem itself is not formalized
Lean 4 / Mathlib: a bounded past-measurable coefficient times independent centered noise has conditional mean zero and a factored second moment
Lean 4 heat-kernel estimates and Gaussian-tempered rough initial data, with source-bound verification receipts.
Partial Lean 4 formalization of Chemotaxis III: stationary estimates, modes, compactness and conditional bifurcation results
To associate your repository with the lean-pkg topic, visit your repo's landing page and select "manage topics."