>>531 この>>506が言っている3行は事実。証明と定理がラムダ計算の式と型に対応しているという理論(Curry-Howard対応)
を使えば、ある文字列(式)がどのような定理(型)を証明しているか、それとも間違っている(型エラー)か自動判定することができる。

しかし、逆に、定理(型)からその証明(式)を導くことは完全自動では無理。