A repository documenting Erdős problems with their statements, status (open, claimed, or solved), related results, and formal proofs in Lean. The collection, curated from Thomas Bloom's catalog, includes problem pages, a library of cited sources, and verification tiers for claimed results.