4 ms·
Ok… has this been verified? I see no publication or at least an announcement on Harmonics webpage. If this is a big deal, you think it would be a big deal, or i
by wasmainiac 11mo ago
Ok… has this been verified? I see no publication or at least an announcement on Harmonics webpage. If this is a big deal, you think it would be a big deal, or is this just hype?
- singularity2001 11mo agoverified by lean so 99.99% yes
- cluckindan 11mo agoLean 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 https://www.erdosproblems.com/forum/thread/124#post-1899
- wasmainiac 11mo 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.
- aaomidi 11mo agoIs there some good literature to read about lean? First time I’m hearing about it and it seems pretty cool.
- anon291 11mo agoAnything in type theory. Lean is fundamentally a strongly typed dependently typed programming language. Start with Haskell and keep going.