Machine-checked statistical learning theory in Lean 4: empirical-Bernstein and time-uniform PAC-Bayes, Markov risk, Rademacher/VC, and Dudley chaining.
The intent of this repository is to build a database of control theoretic proofs in lean.
MathTensor Lean 4 formalizations of Putnam 2025 problems, with machine-verified Mathlib proofs.
A comprehensive formalization of Game Theory in the Lean 4 proof assistant
University Master Thesis
A complete navigation index for every one of Mathlib4's 9,150 modules — plain-English descriptions, systematic disambiguation of similarly named modules, and five deliverables: JSON, RAG export, Claude Skill, spreadsheet, and website.
Kleene algebra, KAT, and relation algebra in Lean 4 / Mathlib, with completeness proofs and proof-producing tactics. Based on Damien Pous’s relation-algebra library.
Simplify arithmetic expressions of ENNReal numbers in Lean4
Formally verified MBSE framework in Lean 4 — dependent type semantics for SysML v2 / KerML with V&V matrix completeness by type checking
Formal verification of the logical incompatibility between the P=NP hypothesis and the Witten-Helffer-Sjöstrand tunneling theorems in spectral geometry. Implemented in Lean 4.
Formally verified modular-forms mathematics in Lean 4 + Mathlib: Ramanujan's τ function, his congruence τ(n) ≡ σ₁₁(n) (mod 691), and kernel-decided nonvanishing τ(n) ≠ 0 for all n ≤ 65536, toward Lehmer's conjecture.
APM-installable agent skills for Lean 4 and Mathlib4 — proof tactics, math domains, review and research workflows, generic tooling.
Formalised mathematics in Lean 4.
Lean 4 formalizations of results from my research on graphs, networks, and the modulus of families of objects.
Retrieval-grounded reviewer-memory tool over closed-PR review history of leanprover-community/mathlib4. Indexes ~158k past reviewer comments across ~35k closed PRs to flag concerns past reviewers have raised before.
Lean 4 formalization of ord_{2^t}(3) = 2^{t-2} and supporting lemmas for Collatz analysis
Machine-checked Lean 4 formalization of TSP complexity barriers, Held-Karp integrality gap (Petersen graph), and Christofides 3/2-approximation (0 sorries).
Visualizer for mathlib library inspired in https://github.com/Crispher/MathlibExplorer . The idea is to connect each topic based on standard curricula to each file in mathlib so new code and math topics can be implemented faster.
Lean 4 formalization of Gleason's theorem via Busch's effects formulation
To associate your repository with the mathlib4 topic, visit your repo's landing page and select "manage topics."