Follow

b-mehta.github.io/unit-fractio – formalization in Lean of Thomas Bloom's proof of the density version of the Erdős–Graham problem, en.wikipedia.org/wiki/Erd%C5%9, according to which every set of integers with positive upper density includes the denominators of an Egyptian fraction representation of one. Via twitter.com/XenaProject/status

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

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

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