Proofs of Erdős problems. Each proof has been carefully checked for correctness with the help of AI. Some have also been formalized and machine-checked in Lean, and formalization of the rest is in progress.