無矛盾であれ

定理証明支援系の無矛盾性とか,示せたとしてどんな規模の証明になるんだろう,とかいう話をした.