(19) A Proof Assistant with Commutative Diagram Interface

The importance of user interfaces for formal theorem prover are now recognized. In category theory, commutative diagrams are extensively used to help understand (informal) proofs written in natural language and logical formulae. So, it seems natural to require the use of commutative diagrams in formal theorem proving in category theory too. In fact, the difficulty in understanding formal proof is one of the major obstacles in formal mathematics, so assistance in obtaining an intuitive idea of what is written would be of great value. Therefore, we are developing a user interface for proof assistant systems, based on commutative diagrams.