alt Hacker NewsHad no idea this was what lean looked like- that's mind blowing. I'm not even sure how someone would critique this if they wanted to
Had no idea this was what lean looked like- that's mind blowing. I'm not even sure how someone would critique this if they wanted to
The point of lean proofs (as it stands) is simply one bit of information: that a given mathematical statement is indeed true.
It's a way to be absolutely certain (modulo bugs in the lean kernel) that a proof you came up for a statement is indeed correct. It is really not meant to be analyzed, much less now that they are fully llm written.