Machine-Verified Bridge: Erdős Problems 699 and 961 Formalized in Lean 4

This paper presents the first Lean 4 formalization of classical Sylvester-Schur theorems, providing machine-verified proof that Erdős problems 699 and 961—two distinct mathematical formulations—are logically equivalent. Leveraging Rei-AIOS AI-assisted verification and computational techniques, it demonstrates how automated theorem provers can connect classical results with modern formal systems. The work opens a pathway for completing the general proof, advancing both automated mathematics and formal verification of mathematical knowledge.