Aristotle from HarmonicMath has solved Erdős Problem 124 in LEAN xenaproject.wordpress.com 1 points by unprovable 2 hours ago