Nice separation of levels in this comment. It’s essential to point out the difference between what can be done by the automated proof-checker and what can be shown ‘from the outside’ about the operation of the proof-checker.
I second DanielVarga: you should incorporate this discussion into the post itself, since it’s exactly the part that people get stuck on.
Nice separation of levels in this comment. It’s essential to point out the difference between what can be done by the automated proof-checker and what can be shown ‘from the outside’ about the operation of the proof-checker.
I second DanielVarga: you should incorporate this discussion into the post itself, since it’s exactly the part that people get stuck on.