3 ms·
You 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 commun
by seanhunter 22d ago
You 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 22d agoWell, Lean needs to get its act together to fix the bugs.
- seanhunter 21d 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.