Claims

../

1977_08_01_barbeau: Barbeau's 1977 list of 101 distinct products of two distinct primes whose reciprocals sum to 1, the first representation of 1 by two-prime denominators; the instance a/b = 1 only, in a problem-solving journal.

1978_08_01_johnson: Johnson's 1978 letter listing 48 distinct products of two distinct primes whose reciprocals sum to 1, answering Barbeau's question for the fewest terms with the record that stood until 2020; the instance a/b = 1 only.

2020_09_01_watanabe: Watanabe's 2020 preprint printing seventeen representations of 1 as a sum of 47 reciprocals of distinct products of two distinct primes, the shortest known; the instance a/b = 1 only, with an outside Lean certificate of one.

2026_06_13_li: Li's preprint of June 2026 proving that every natural number, and every a/b with b squarefree above an explicit threshold at most 1/5, is a sum of distinct unit fractions with semiprime denominators; partial, unrefereed.

2026_06_19_tang: Tang's Lean 4 development of June 2026, released on Zenodo, asserting the whole statement with two Rosser-Schoenfeld bounds taken as axioms, and his manuscript frozen in August 2026 and published in October 2026.

2026_09_26_li: Li's preprint of September 2026 asserting that every positive rational with squarefree denominator is a sum of distinct unit fractions with semiprime denominators, with a Lean 4 formalization; the site's one full proof claim.

---