Claims

../

1985_06_01_monier: The published solution of Monthly Problem 6447 by Jean-Marie Monier (1985), credited with n_k <= k! for k >= 3 and a proof of the Erdős–Selfridge exception; refereed in The American Mathematical Monthly.

2026_07_25_white: A repository of 25 July 2026 by Patrick White, with a construction by GPT-5.6 Sol, claiming n_k <= exp(C k log log k / log k) for all large k; not posted to the site's forum and unreviewed.

2026_07_27_cipollini: A proof claim posted to the site's proof-claim tab on 27 July 2026 asserts that log n_k is at most (k / log k)(log log k + log log log k + log 2 + o(1)); the write-up requires a sign-in, and the claim is unreviewed.

2026_08_04_cipollini: A proof claim posted to the site's proof-claim tab on 4 August 2026 asserts that log n_k is at least c (log k)^2, a superpolynomial lower bound on n_k; the write-up requires a sign-in, and the claim is unreviewed.

2026_10_01_leap: A Lean 4 proof of 1 October 2026 by the LEAP prover agent that n_k is O(exp((k/log k)(log log k + log log log k + log 2))), little-o of Cambie's bound, linked by formal-conjectures as a variant's formal proof.

---