For context and why this interesting: "Abstract. This report gives case studies supporting the hypothesis that it is often affordable for a paper presenting th

For context and why this interesting: "Abstract. This report gives case studies supporting the hypothesis that it is often affordable for a paper presenting theorems to also include proofs that have been checked with today’s proof-checking software."