Write an essay (3000-4500 characters in Japanese
or 1000-1500 words in English) about the differences
between writing and explaining mathematical
theorems and their proofs using natural language
and a formal language and mechanical proof checker
like Mizar.
For each point of discussion, provide a concrete example.
