4 ms·
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 certa
by frotaur 8d ago
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.
- aizk 8d agoWell, 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.