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

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.

Simplify arithmetic expressions of ENNReal numbers in Lean4

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

Formally verified MBSE framework in Lean 4 — dependent type semantics for SysML v2 / KerML with V&V matrix completeness by type checking

Solving Hilbert's 6th problem in Lean

Lean 4 formalization of Gleason's theorem via Busch's effects formulation

Lean 4 formalization of ord_{2^t}(3) = 2^{t-2} and supporting lemmas for Collatz analysis

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 / 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).

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.

29,750 competition-math proofs migrated from Lean 4.8 to Lean 4.27 with 60K traced tactic pairs

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

Lean Proofs for Admissible Structure Theory

A Lean 4 formalization of discrete causal posets and convex-cone models for AQEI constraints. Features 130+ machine-checked theorems covering chain-complex homology proxies, $Z_1$ cycle space stability, and bidirectional equivalence of 1-cycle proxies.

Lean 4 formalizations of results from my research on graphs, networks, and the modulus of families of objects.

We carry out a complete formalization of the spectral theorem in Lean, for both bounded and unbounded linear operators over some Hilbert space H.

autogenerated tactics list for mathlib4