Many textbook proofs are essentially human-readable representations of natural deduction proofs. Terms in dependent type theory provide formally checkable representations of natural deduction proofs. We show how the new mathematical assistant system Scunak can be used to verify a textbook proof by translating the LATEX. version into a proof term in a dependent type theory. We also show how Scunak can give interesting output upon failure.
展开▼
