>>442
そもそも、数学者にとって論理とは、
証明を記述するための規則でしかない。

それはともかく、カリー・ハワードも原形は素朴なものだが。

それから、数学者は証明の記述にヒルベルト流の体系なんて
用いてないし、用いろといっても無理だろう。
ゲンツェン流の自然演繹ならまだ話はわかるが、実際の証明は
計算機でも処理できるほど完璧に書かれてるわけではない。
そんなことしてたら、証明書き終わる前にくたばっちまうｗ