Follow – formalization in Lean of Thomas Bloom's proof of the density version of the Erdős–Graham problem,, according to which every set of integers with positive upper density includes the denominators of an Egyptian fraction representation of one. Via

The blueprint appears to show Theorem 2 of as verified, but Theorem 3 (log density) still to go.

· · Web · 0 · 1 · 3
Sign in to participate in the conversation

The social network of the future: No ads, no corporate surveillance, ethical design, and decentralization! Own your data with Mastodon!