Claims

../

2026_09_03_adamczewski: A disproof found by GPT-6 Astra in Epoch AI's benchmark, with a public Lean development from Tom Adamczewski: no constant c > 0 makes N > c 2^n hold for every sum-distinct set of n integers in {1, ..., N}; accepted on Lean built here.

2026_09_15_alexeev: A second Lean 4 disproof in Boris Alexeev's lean-proofs repository, credited to GPT-6 Astra, giving for every n at least 2 a sum-distinct n-set in {1, ..., N} with N below 2^(n+1)/log_2 n, and a cube-root saving; accepted.

---