Claims

../

1950_01_01_erdos: Erdős's 1950 paper proves N(a,b) < c_1 log b / log log b for every a/b and N(b-1,b) > log log b - 1, with the average of N(a,b) over a above half of log log b - 1, so log log b << N(b) << log b / log log b; refereed.

1985_01_01_vose: Vose proves that every a/b < 1 is a sum of O(sqrt(log b)) distinct unit fractions, so N(b) << sqrt(log b), replacing Erdős's log b / log log b; refereed in the Bulletin of the London Mathematical Society.

2026_09_01_thepriceisright: A Lean proof, produced by Harmonic's Aristotle prover and published by the GitHub account thepriceisright, of the formal-conjectures variant lower_1950 of Problem 304: log log b <= 6 N(b) for b >= 3; claimed.

2026_09_16_van_doorn: Theorem 1.2 of the note by Wouter van Doorn and GPT-6 Astra Pro, posted on 16 September 2026 on Problem 18's proof-claims tab: every a/b with b large is a sum of at most 2c0 (log log b)^2 distinct unit fractions, c0 = 14/log 2.

2026_09_25_openai: The OpenAI mathematics release's Theorem 1.1 of 25 September 2026, that every a/b with 1 <= a < b is a sum of at most c log log b distinct unit fractions, accepted on the Lean declarations the corpus's verification built and audited.

---