Comment by jgbuddy
20 hours ago
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
20 hours ago
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.
Well, how do we know there aren't errors in their construction within the lean code? Does it just "not compile" or something, or is it deeper / more fundemental than that.
https://ammkrn.github.io/type_checking_in_lean4/trust/trust....
that's essentially it, if the proof is incorrect it does not compile which signifies a problem in some step.