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
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.
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.
Lean 4 (v4.34.1 / Mathlib) formalization of noncommutative information geometry, Peirce-Weyl units, Drazin-Moore-Penrose spectral splittings, Jordan-Lie operator algebras, and categorical inductive colimits.
Machine-checked Lean 4 formalization of TSP complexity barriers, Held-Karp integrality gap (Petersen graph), and Christofides 3/2-approximation (0 sorries).
Lean proofs, reproduction programs and frozen evidence behind a family of research papers
Formalised mathematics in Lean 4.
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
Lean 4 formalizations of results from my research on graphs, networks, and the modulus of families of objects.
To associate your repository with the mathlib4 topic, visit your repo's landing page and select "manage topics."