What is a Formal Proof? https://golem.ph.utexas.edu/category/2016/08/what_is_a_formal_proof.html http://math.andrej.com/2016/08/09/what-is-a-formal-proof/ 定理証明系における型検査って別に決定可能でなくても良くね？という話。 Andrej Bauer の Andromeda (元 Brazil) はその発想が根本にある。