ああ…
>>77で形式的証明を与えることが重要なんではなく
これまでも主張しているように
数学的常識を疑う思考ができない人がIUTを理解できないのだから
その障壁を取り除くのにLeanはコミュニケーションツールとして有益という謎の主張をしてるのは
>>32
単に形式的証明を与えるだけだとショルツェの二番煎じになっちゃうからか
対抗意識が強いんだね

この発表聞いた人は頭抱えただろうな
数学の発表じゃないし
形式的証明与えたらもうコミュニケーションする必要もないんだが
一方的に宣言すればいい
勝利したと