There are now sufficiently many different examples of Erdos problems that have been resolved with various amounts of AI assistance and formal verification (see https://github.com/teorth/erdosproblems/wiki/AI-contributions-to-Erd%C5%91s-problems for a summary) that one can start to discern general trends.
Broadly speaking, we now see an empirical tradeoff between the level of AI involvement in the solution, and the difficulty or novelty of that solution. In particular, the recent solutions have spanned a spectrum roughly describable as follows:
1. Completely autonomous AI solutions to Erdos problems that are short and largely follow a standard technique. (In many, but not all, of these cases, some existing literature was found that proved a very similar result by a similar method.)
2. AI-powered modifications of existing solutions (which could be either human-generated or AI-generated) that managed to improve or modify these solutions in various ways, for instance by upgrading a partial solution to a full solution, or optimizing the parameters of the proof.
3. Complex interactions between humans and AI tools in which the AI tools provided crucial calculations, or proofs of key steps, allowing the collaboration to achieve moderately complicated and novel solutions to open problems.
4. Difficult research-level papers solving one or more Erdos problems by mostly traditional human means, but for which AI tools were useful for secondary tasks such as generation of code, numerics, references, or pictures.
(1/2)