3 ms·
That particular quote isn't questioning Lean, but "convert[ing] the proof into inputs for Lean." GIGO
by hyperthesis 3y ago
That particular quote isn't questioning Lean, but "convert[ing] the proof into inputs for Lean." GIGO
- SkiFire13 3y agoThat's not how it works. If you input garbage in Lean or other proof checker they will just tell you it's wrong. You would have to input garbage in the statement you want to prove for them to accept a wrong proof (which must still be correct for that garbage statement!). To rule this out you just have to manually check the translation of the statement, which is most often much much smaller than the proof itself.
- hyperthesis 3y agoYou disagree then agree. Here's an elaboration of the point: https://news.ycombinator.com/item?id=37341439 https://news.ycombinator.com/item?id=37341439