I would like to request review of a possible AI-contributions wiki entry for Erdős Problem #425.
Suggested placement: Section 1(d), "AI collaborating with humans"
Proposed row:
| Problem |
Humans |
AI systems |
Date |
Outcome |
| [425] |
Kenta Kitamura |
Claude Code / Claude Fable 5, Codex 5.5, ChatGPT 5.5 Pro |
6--11 Jun, 2026 |
🟡 Improved explicit lower bound c < 3.499 for the multiplicative Sidon lower bound, with Lean formalization |
Forum discussion:https://www.erdosproblems.com/forum/thread/425
Repository:https://github.com/KitaKen1/erdos-425-lower-bound-3499-attempt
This is an update/improvement to the currently recorded #425 AI-contributions entry: the bound is improved from the earlier 2.951... layered construction to c < 3.499, with Lean formalization under PNT.
If the editors think this belongs in a different section or should be phrased differently, I would be grateful for guidance.
I would like to request review of a possible AI-contributions wiki entry for Erdős Problem #425.
Suggested placement: Section 1(d), "AI collaborating with humans"
Proposed row:
Forum discussion:https://www.erdosproblems.com/forum/thread/425
Repository:https://github.com/KitaKen1/erdos-425-lower-bound-3499-attempt
This is an update/improvement to the currently recorded #425 AI-contributions entry: the bound is improved from the earlier 2.951... layered construction to c < 3.499, with Lean formalization under PNT.
If the editors think this belongs in a different section or should be phrased differently, I would be grateful for guidance.