A Generalized Trace Reconstruction Problem: Recovering a String of Probabilities
Formalizes the lower bound for the generalized trace reconstruction problem of recovering a string of probabilities from random traces.
A Sharp Version of Talagrand's Selector Process Conjecture and an Application to Rounding Fractional Covers
Formalizes a sharp version of Talagrand's selector process conjecture and its consequence for rounding fractional covers to integral ones.
Approximation Guarantees of the Median Mechanism in ℝᵈ
Formalizes the dimension-independent approximation ratio of the coordinate-wise median mechanism in ℝᵈ.
Efficiently Learning Mixtures of Two Gaussians
Formalizes that the first six moments of a one-dimensional mixture of two Gaussians suffice to robustly recover its parameters.
Refuting the Direct Sum Conjecture for Total Functions in Deterministic Communication Complexity
Formalizes a counterexample refuting the direct sum conjecture for total functions in deterministic communication complexity.
A Proof of the Cycle Double Cover Conjecture
Formalizes a proof of the cycle double cover conjecture — every finite bridgeless graph has a collection of cycles covering each edge exactly twice — reducing it to an elementary linear-algebra argument over 𝔽₂³.
Planar Point Sets with Many Unit Distances
Formalizes the disproof of Erdős's unit-distance conjecture: an infinite unramified 3-tower of totally real fields yields n-point planar sets with ν(n) ≥ n^{1+δ} unit distances for infinitely many n.
The Strong Perfect Graph Theorem
Formalizes the strong perfect graph theorem — a graph is perfect if and only if it is Berge — through the paper's structure theorem: every Berge graph is basic, or one of it and its complement admits a proper 2-join, or it admits a proper homogeneous pair or a balanced skew partition. The main theorem is sorry-free with only Lean's three foundational axioms.