background image

22.2. FORMALIZING THIS THEORY

385

Thus it would be good to formalize the theory presented in this book in a proof

assistant

1

such as Coq.

If you want to work on formalizing this theory, please let me know.

See also

https://coq.inria.fr/bugs/show_bug.cgi?id=2957

1

A

proof assistant

is a computer program which checks mathematical proofs written in a

formal language understandable by computer.