I have used Claude and Gemini to formalize conjectures for all remaining Erdos problems from https://github.com/teorth/erdosproblems
This is marked as a key milestone in the DeepMind Formal Conjectures repo: https://github.com/google-deepmind/formal-conjectures/milestone/1
