Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.
Updated
Claims
2026_02_10_he_tang: He and Tang's 2026 paper, with results found using ChatGPT-5.2 Thinking, computing the Erdős–Trotter thresholds n_0(2) = 3 and n_0(3) = 8 and proving 2r + 2 <= n_0(r) <= 2r + 2 log_2 r + O(log log r) for r >= 4; pending.
2026_07_17_thiim: Thiim's 2026 manuscript, written with language models, determining the Erdős–Trotter threshold as 2r+4 for 4 <= r <= 10 and 2r+5 for r >= 11, with a Lean development; with He and Tang's small cases it completes the table.
2026_07_21_ronen: Ronen's 2026 write-up, drafted and audited with AI systems, proving that n_0(4) = 12: no admissible family with n-3 sizes at n = 12, explicit families for 13 <= n <= 19, and He and Tang's construction beyond; pending.