>>434-442
>いずれにせよこれで一段落ということにしてはどうか
>suspendedと思った者は皆無に等しい

ID:5zPtkw66 は、御大か
巡回ありがとうございます
コメントありがとうございます。

１）まあ、それをリアル界で決めるのは、望月・星氏らでしょう
　ここは、バーチャル 場末の５ｃｈです
２）私見ですが、先週7/17金のLANAプロジェクトの中間発表は
　3.11→3.12導出が 現状ではLean形式化に乗らなかったが
　可能性は残っているという
３）その可能性とは、おそらく 遠アーベルのLeanライブラリー不足で
　Leanライブラリーを 何らか追加するとか
　あるいは別に、3.12そのものではなく 3.12をなんらか変形して IUT IVを導けるようにすること
４）さて、まずこの状況（中間発表）を受けて、望月・星氏らが彼ら自身の見解と見通しを発表すべきでしょうね
　というのは、日仏合同の Arithmetic & Homotopic Galois Theory IRN 共同研究プロジェクトが走っている https://ahgt.math.cnrs.fr/activities/
　ここには、日本の予算もさることながら 仏の予算も入っている。その落とし前が必要となる
５）ところで 数学では「数列の収束加速法」が、古代から研究されている （＾＾
　いまの場合、事態の収束加速法は、事実を隠さずにオープンにして 議論することですね
　Leanコードも隠さずに、オープンにして 議論することが、収束加速の要諦でしょう！

(参考)
https://ja.wikipedia.org/wiki/%E6%95%B0%E5%88%97%E3%81%AE%E5%8A%A0%E9%80%9F%E6%B3%95
数列の加速法
収束の遅い数列を収束の速い数列に変換するアルゴリズムの総称である[1]
歴史
19世紀以前
ヨーロッパと日本で研究が始まった。古典的な二つの加速法はオイラー変換[2] と クンマー変換である。日本では関孝和、建部賢弘など、ヨーロッパではアイザック・ニュートンなどが取り組んだ[3]。