https://b-mehta.github.io/unit-fractions/ – formalization in Lean of Thomas Bloom's proof of the density version of the Erdős–Graham problem, https://en.wikipedia.org/wiki/Erd%C5%91s%E2%80%93Graham_problem, according to which every set of integers with positive upper density includes the denominators of an Egyptian fraction representation of one. Via https://twitter.com/XenaProject/status/1536099892694859777
The blueprint appears to show Theorem 2 of https://arxiv.org/abs/2112.03726 as verified, but Theorem 3 (log density) still to go.
The social network of the future: No ads, no corporate surveillance, ethical design, and decentralization! Own your data with Mastodon!