mathlib4

Zero-sorry Lean 4 library of finite-sample statistical learning theory: PAC-Bayes (incl. a five-component test-time meta-bound), VC, Rademacher, sharp McDiarmid, and Dudley chaining. ICML 2026 AI4MATH

MathTensor Lean 4 formalizations of Putnam 2025 problems, with machine-verified Mathlib proofs.

University Master Thesis

Simplify arithmetic expressions of ENNReal numbers in Lean4

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.

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

Formalised mathematics in Lean 4.

APM-installable agent skills for Lean 4 and Mathlib4 — proof tactics, math domains, review and research workflows, generic tooling.

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.

Solving Hilbert's 6th problem in Lean

Lean 4 formalization of fundamental physics: PPN metric, LLI satellite bounds (SaToR-G), and Quantum Mechanics in Hilbert spaces.

DST-Vault / TDI Loop Quantum Gravity: Formal verification of gravitational wave constraints and entropy area law corrections in Lean 4

Axiomatic framework for Dual Sets Theory (DST) and Bio-Resonance in Lean 4

Hypernatural Numbers in Lean 4 (With the proof of Łoś's Theorem)

Lean Proofs for Admissible Structure Theory