証明って公理の有限回の適用じゃね?
だったら理論上計算機で実現できるんじゃね?