Repositories & Publications

Papers, and the Lean formalization projects I maintain.

Publications

Optimal Sparse Bounds and Commutator Characterizations Without Doubling

F. D'Emilio, Y. Lin, N. A. Wagner, B. D. Wick · 2025

preprint arXiv:2510.26505

Repositories

Besicovitchs-1-2

Lean 4 + Mathlib

A machine-checked proof that the planar rectifiability threshold satisfies $\tfrac12\le\sigma_1(\mathbb{R}^2)\le 0.6934$.

Everything else is on GitHub.