3 ms·
Skill issue. Also lean is meant to be executed, not read.
by rfgplk 25d ago
Skill issue. Also lean is meant to be executed, not read.
- arodev 25d agoi think they're talking about the writeup
- oinoom 25d agoits important to read it anyway because there have been and will continue to be errors in the construction of the proof software itself. which leads ai and humans alike to prove things that arent true
- professoretc 25d agoA proof is not like a program. The goal of a program is to "do the thing", thus you can make the argument that it doesn't matter what the code looks like as long as its works right. But the goal of a proof isn't to "do the thing" (where "the thing" is just to print Yes or No), it's to communicate. An unintelligible proof is really just a first draft.
- Jblx2 25d ago>A proof is not like a program. https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...