For context, Terence Tao started a wiki page titled “AI contributions to Erdős problems”: https://github.com/teorth/erdosproblems/wiki/AI-contribution... (as mentioned in an earlier post https://mathstodon.xyz/@tao/115818402639190439) — even relative to when he started this page less than two weeks ago (Dec 31), the current result (for problem [728]) represents a milestone: it is the first green in Section 1 of that wiki page.
Very interesting that the vast majority of proofs formalized by AI (section 6) were only completed in the last few months. Exciting times ahead!