| ▲ | jgbuddy 8 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 | |||||||||||||||||
| ▲ | frotaur 8 hours ago | parent [-] | ||||||||||||||||
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. | |||||||||||||||||
| |||||||||||||||||