FormaliaXiv

Formalizes the lower bound for the generalized trace reconstruction problem of recovering a string of probabilities from random traces.

Formalizes a sharp version of Talagrand's selector process conjecture and its consequence for rounding fractional covers to integral ones.

Formalizes the dimension-independent approximation ratio of the coordinate-wise median mechanism in ℝᵈ.

Formalizes that the first six moments of a one-dimensional mixture of two Gaussians suffice to robustly recover its parameters.

Formalizes a counterexample refuting the direct sum conjecture for total functions in deterministic communication complexity.

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 𝔽₂³.

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.

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.

Formalizes Babai's quasipolynomial-time algorithm for Graph Isomorphism and String Isomorphism — including the Design Lemma, Split-or-Johnson, the Main Structure Theorem for alternating quotients, Local Certificates, and the Master Algorithm on an explicit random access machine, together with an explicit running-time bound of exp(O((log N)⁵)). The formalization is sorry-free and rests only on five cited group-theoretic theorems.