Checking machine-checked proofs
I happen to serve on a regular basis as a reviewer for submissions dealing with formalized mathematics. These submissions often consist of regular papers, accompanied with the source code of a library of formal proofs. This source code is meant to be machine-checked with a certain proof assistant. Inspecting a…
