「3.11→3.12のところを、計算機が追える厳密な形に落とせなかった」なら、少なくともその箇所は現行の形式化手法では証明の鎖として確定できなかった、ということです 。ただし、これはそのままIUT理論にギャップがあると確定したことと同義ではありません 。
形式化できない、というのは通常、
• 定義がまだ十分に機械可読な形に整理されていない。
• 前提や同一視のルールが暗黙で、コード化しきれない。
• 途中の変換に必要な補題が不足している。
• のどれか、あるいは複合です 。したがって「証明が偽だった」と直結するわけではなく、「現時点で検証可能な形に再構成できない」という意味合いが強いです 。
3.11→3.12に限ると
この箇所は、抽象的な比較不等式を、ABC予想に使える具体的な不等式へ移す橋渡しでした 。そこが形式化できない場合、疑われるのは主に次の点です。
• どの量を同一視してよいかの規則が曖昧。
• 変換前後で不等式の向きや誤差項が保存されているか不明。
• 「復元」や「遠アーベル的対応」を前提にしたステップが、機械的には未整備。
どう解釈すべきか
数学的には、「証明の核心部分を、独立に再現可能な公理的記述へ分解できていない」という状態です 。これは重い意味を持ちますが、同時に形式化プロジェクトでは珍しくありません。特にIUTのように概念層が多い理論では、まず人間が理解している説明を、機械が扱える細部まで分解する作業自体が大仕事です 。
「3.11→3.12は形式化不能」なら、少なくともその現行の定式化では、証明の最後の接続点が閉じていないことを示します 。ただし、その原因は「理論の誤り」だけでなく、「記述不足」「補題不足」「翻訳の設計ミス」でも起こります 。なので、結論としてはギャップの疑いを強める材料にはなるが、単独で致命傷とは言えない、という見方が妥当です 。