Email Gateway (Aug 22 2022 at 15:40): Email Gateway (Aug 22 2022 at 15:40):From: Colin Rowat <c.rowat@espero.org.uk>
Dear Scott,
To address a broader question than the one you asked, you might like Mark
Adam's proof auditing paper, if you've not seen it:
http://www.proof-technologies.com/flyspeck/qed_paper.pdf
It looks at ways in which theorem provers might provide false assurances
(even in the absence of smuggled 'sorry' statements).
Best,
Colin
Last updated: Apr 20 2024 at 04:19 UTC