FormaliaXiv

Formalized papers with bidirectional PDF ↔ Lean cross-references.

The framework behind this site

Beyond the Library

An Agentic Framework for Autoformalizing Research Mathematics

Arshia Soltani Moakhar · Iman Gholami · Max Springer · Mahdi JafariRaviz · MohammadTaghi Hajiaghayi

University of Maryland · Princeton University

Read the paper on arXiv ↗

Formalized papers

A Generalized Trace Reconstruction Problem: Recovering a String of Probabilities
STOC 2025 · Joey Rivkin, Gregory Valiant, Paul Valiant
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
STOC 2025 · Huy Tuan Pham
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 ℝᵈ
STOC 2025 · Nick Gravin, Jianhao Jia
Formalizes the dimension-independent approximation ratio of the coordinate-wise median mechanism in ℝᵈ.
Efficiently Learning Mixtures of Two Gaussians
STOC 2010 · Adam Tauman Kalai, Ankur Moitra, Gregory Valiant
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
STOC 2025 · Simon Mackenzie, Abdallah Saffidine
Formalizes a counterexample refuting the direct sum conjecture for total functions in deterministic communication complexity.
A Proof of the Cycle Double Cover Conjecture
OpenAI note (2025) · OpenAI
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
OpenAI note (2026) · OpenAI
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.