Machine-verified statistical learning theory in Lean 4. 57 FormalSLT modules: sharp McDiarmid bound, conditional sub-Gamma MGF extractor, unit-interval finite-net Dudley bridge, finite PAC-Bayes confidence bounds. Zero sorry, zero admit, no custom axioms.

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

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.

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

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

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

Lean on Goldbach's conjecture

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.