Harmonic's automated theorem prover Aristotle solves open Erdős problem in Lean

Vlad Tenev tweeted about it here: https://x.com/vladtenev/status/1994922827208663383

This is amazing! We live in wonderful times!