4 ms·
You don't need to read the lean proof for that, only the statement.
by eru 1mo ago
You don't need to read the lean proof for that, only the statement.
- seanhunter 1mo agoYou need to read the lean proof (not just the statement of the proposition) to assess whether the proof is honest. The link I provided is the lean prover community firstly officially agreeing with that claim and secondly explaining why that is the case.
- eru 1mo agoWell, Lean needs to get its act together to fix the bugs.
- seanhunter 1mo agoThey’re working on it, but the bulk of the effort goes into making it more useful to working mathematicians rather than resisting malicious proof attempts.