26/08/06 07:54:42.53 yU/2F8x4.net
>>824のつづき
LANAのような形式化プロジェクトの意義はここにあります。形式化では、
定義は何か
どの対象からどの対象への写像なのか
どの仮定を使っているのか
どの推論規則で結論が出るのか
を極端に明示する必要があります。
その過程で、「あれ、この部分は人間同士が暗黙に補っていたのでは？」という箇所が浮かび上がります。
逆に言えば、形式化できれば「問題なし」と確認される可能性もあります。
なので質問の、
要するに肝心な点が全然理解されないまま？
については、
「少なくとも論争の核心部分について、数学界全体で共有された理解にはまだ達していない」
というのが近いです。
ただし、
望月氏とその支持者は「理解されていないのは批判側」と考えている
Scholze・Stix側は「理解した上で核心部分に問題がある」と考えている
ので、「誰も理解していない」というより、高度に専門的な部分について、理解の仕方が対立しているという状態です。