>>205 補足
>その差を考えずに
>”証明をコードに直す形式化は、複雑な式をコードに翻訳する骨の折れる作業で
ケプラー予想の場合は数十人で約10年かかった”
>と書いた部分が、”事実の確認”不足だぞと

個人の感想ですが
１）文章表現部分は、コード化しやすい気がする
２）問題は、圏論的に 矢印図で 文章表現部分になっていない部分
　例えば、下記の ”素数ストリップ D”とか
　ポンチ絵表現があった
　これを言語化しないと、コード化できないだろう

ここらが、IUTのコンピューター検証で 難しいところだと
思っています

(参考)
イタリア語版
https://it.wikipedia.org/wiki/Teoria_di_Teichm%C3%BCller_inter-universale
IUT
(google訳)
4つの論文の発表
IUTeich I: ホッジ劇場の建設
最初の論文はA4 PDF形式で183ページ
略
素数ストリップ D と「カプセル」の概念は、両方の基本的な接着ホッジ劇場の構成要素である。これらの構成要素は、望月によって「局所オブジェクト」、「大域オブジェクト」、そして「ブリッジ」（カプセルを素数ストリップDと大域オブジェクトに接続するため、このように呼ばれる）と呼ばれる。2つのホッジ劇場（算術ホッジ劇場と幾何ホッジ劇場）間の接着は、NF-ホッジ劇場のΘ ±を形成するために、関数アルゴリズムを通じて「Θブリッジ」と呼ばれる2つのブリッジで正確に行われる。生成される接着同型は一意であり、多重ではない。[ 30 ]