ひと月以上前（4月6日）「自然言語混じり形式証明の意味論」という記事を書きました。そこに、5つの過去記事へのリンクがあります。それら一群の記事で、「自然言語文がコメントや補足説明ではなくて、形式証明の正式な一部となるような証明記述言語が使える…