>>392
「ほとんどチェックできない証明ばかりではないですか」の例が四色定理？
こういう定理って数学の定理のごくごく一部だと思ってたけど。

＞コンピュータの自動証明に関係してればありうるでしょ。
飽くまで彼らが研究してるのは自動証明のプログラム自体であって、
自然数論も扱えないような体系自体を研究してるわけじゃないですよ。

＞＞philosophically weakで何がmathematically uglyなのかな、と思って聞いてみた
＞タルスキーは直観主義について上の言葉で論評したとき例をあげたのですか？
Tarskiは直観主義についてどう思うか？と聞かれたから、
「直観主義は」哲学的には弱く、数学的には醜悪である、と答えたんでしょ。
それがどういうものかは別に例を挙げなくとも聞いたほうも答えたほうも分かっていました。
Tarskiが指していたものは明確です。

それに対して「あの言葉はそっくりタルスキーにお返しできるとおもうのですが。」
というレスがあった。これは指すものが不明確です。
例えばBanach-Tarskiの定理なんかの事を言っているのかもしれないし
全然関係ないのかもしれない。でも数学と哲学に跨るようなTarskiの業績について言っているのは間違いないだろう。
だからTarskiの仕事の具体的にどういう部分について言っているのか？と聞いたんだけど。