12/02/04 22:52:20.33
ｽﾚﾘﾝｸ(math板:456番)
>今夜0時までに
>田中の数学基礎論講義の5章までの定理をすべて
>Coqで証明するよ＾＾
もし、数理論理学が
「他人様がすでに自然言語で書いた証明を
計算機でチェックできる言語で書き直す作業」
だとしたら、そんなもんは確かにクソだ。
もちろん、実際の数理論理学は全く異なるわけだが。
12/02/04 22:52:20.33
ｽﾚﾘﾝｸ(math板:456番)
>今夜0時までに
>田中の数学基礎論講義の5章までの定理をすべて
>Coqで証明するよ＾＾
もし、数理論理学が
「他人様がすでに自然言語で書いた証明を
計算機でチェックできる言語で書き直す作業」
だとしたら、そんなもんは確かにクソだ。
もちろん、実際の数理論理学は全く異なるわけだが。