定理証明支援系についてのアドベントカレンダーです。Coq, isabelle, agda, 自作言語等, 題材となる言語に制限はありません。また型理論、圏論、数学基礎論、HoTTなど周辺の分野に関するものも受け付けています。