確かＰ算術とかいう簡単な演算体系の定理を証明するのに非決定性アルゴリズムで2重指数時間かかるという定理があったな。
定理の証明を実際的な時間で証明するのは何らかの支援が必要でしょうな。