Machine-checked statistical learning theory in Lean 4: empirical-Bernstein and time-uniform PAC-Bayes, Markov risk, Rademacher/VC, and Dudley chaining.
MathTensor Lean 4 formalizations of Putnam 2025 problems, with machine-verified Mathlib proofs.
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.
Simplify arithmetic expressions of ENNReal numbers in Lean4
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 MBSE framework in Lean 4 — dependent type semantics for SysML v2 / KerML with V&V matrix completeness by type checking
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 formalization of ord_{2^t}(3) = 2^{t-2} and supporting lemmas for Collatz analysis
Lean 4 formalization of Gleason's theorem via Busch's effects formulation
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.
Automated theorem generalization in Lean
A literature library for Lean4.
Lean 4 formalizations of results from my research on graphs, networks, and the modulus of families of objects.
Lean Proofs for Admissible Structure Theory
Lean 4 / Mathlib formalization of the Spectral Sandwich Theorem and Theorem 7.1 (Wheel as Constrained Fisher–Rao Gradient Flow, leading order) — companion repository for "Spectral Structure on Graph Signal Optimization" (2026).
Axiomatic framework for Dual Sets Theory (DST) and Bio-Resonance in Lean 4
29,750 competition-math proofs migrated from Lean 4.8 to Lean 4.27 with 60K traced tactic pairs
Add a description, image, and links to the mathlib4 topic page so that developers can more easily learn about it.
To associate your repository with the mathlib4 topic, visit your repo's landing page and select "manage topics."