I solved my 3rd Erdős problem, #870, with ChatGPT-5.5-Pro, then verified it by formalizing the whole proof in Lean 4, sorry-free and axiom-free! With about 180,000 lines of Lean code, as far as I can find, no one person has formalized a single problem at this scale. 🧵 1/n
