The 19th Theorem Proving and Provers meetingにて川添、斉藤、津山が定理証明支援系を使った研究について発表します。それぞれLean, Coq, Agdaを使っていて、定理証明支援系の多様性にも挑戦しています 🙂