Recording HOL Proofs in a Structured Browsable Format

摘要

It is possible to discern two attitudes toward proof in the computer science community. Some regard a proof as a formal mathematical object, while the others view proof as a social process: aq proof is an argument that convinces its reader. These views have been largely incompatible.