| ▲ | cluckindan 16 hours ago | |
Lean verified a proof of a solution to a problem, but was it the same problem as Erdős problem #124? | ||
| ▲ | wasmainiac 9 hours ago | parent [-] | |
> My summary is that Aristotle solved "a" version of this problem (indeed, with an olympiad-style proof), but not "the" version. > I agree that the [BEGL96] problem is still open (for now!), and your plan to keep this problem open by changing the statement is reasonable. Alternatively, one could add another problem and link them. I have no preference. — BorisAlexeev There we go, so there is hype to some degree. | ||