cluckindan 3 days ago

Lean verified a proof of a solution to a problem, but was it the same problem as Erdős problem #124?

https://www.erdosproblems.com/forum/thread/124#post-1899

Reply View 1 reply
  • wasmainiac 3 days ago

    > 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.

    Reply View 0 replies
aaomidi 3 days ago

Is there some good literature to read about lean? First time I’m hearing about it and it seems pretty cool.

Reply View 1 reply
  • anon291 a day ago

    Anything in type theory. Lean is fundamentally a strongly typed dependently typed programming language. Start with Haskell and keep going.

    Reply View 0 replies