Inter-universal geometryとABC予想(シン応援スレ) 92

Inter-universal geometryとABC予想(シン応援スレ) 92 (288ﾚｽ)
上下前次 1-新
通常表示 512ﾊﾞｲﾄ分割ﾚｽ栞

229: １３２人目の素数さん [] 2026/07/09(木) 06:26:02.45 ID:vd34l1fj

＿　＿
　　　　　　　　　　　／::.　ｿ . :;;ヽ
　　　　　 ＿　＿.. /::.　　　　 ..::;;ヽ＿　＿　
　　　　／::.　ｿ . :;;ヽ　　　　　 .／::.　ｿ . :;;ヽ
　　　 /::.　　　　 ..:::;;;ヽ　　　 /::.　　　　 ..:::;;;ヽ
　　　/::.　　　　　　..::;;;;ヽ＿ /::.　　　　　　..::;;;;ヽ
　　/::.　　　　　　　 ..::::;;;;⌒/::.　　　　　　　 ..:::;;;;i
　 （::.　　　　　　　　..::;;;丿（::.　　　　　　　　..::;;;丿
　　　>::...＿＿＿..::::;;;イ＝　>:::...＿＿＿..::::;;;イ
　　　!ヾ.￣⌒_＿￣彡|　　. !ヾ.￣⌒_＿￣彡|
　　　iﾐ:::ミＣ＝　≡..:::　） 　.iﾐ:::ミＣ＝　≡..:::. ）
　　　|:::　　　　　″. ´./.l. |　|:::　　　　　″. ´/
　　　|::: （'　　　 （　::;;;|丿ﾉ　|::: （'　　　 （　::;;;|
　　　|:::　| ﾐ　　　ヽ＼||　ﾐ.　|:::　| ﾐ　　　ヽ＼|
　　　|:::　丶ヽ　　..:ヽ　）.　　|:::　丶ヽ　　..:ヽ　）
　　 （ ＼　 l. |　　..:;;;;;;|　 　（ ＼　 l. |　　..:;;;;;;|
　　　|::＼∨丿 ″..:;;;;;| | ﾐ　|::＼∨丿 ″..:;;;;;|
　　　|:::　| ﾐ　　　ヽ＼:|.（　( |:::　| ﾐ　　　ヽ＼:|
　　　|:::　丶ヽ　　..:ヽ　） l. | |:::　丶ヽ　　..:ヽ　）
　　 （ ＼　 l. |　　..:;;;;;;|　　 （ ＼　 l. |　　..:;;;;;;|
　　　|::＼∨丿 ″..:;;;;;| （　(.|::＼∨丿 ″..:;;;;;|
　　　|:::　（　( 　ﾞ　..:;;;;;|.＼.　|:::　（　( 　ﾞ　..:;;;;;|
　　 （ ＼　 l. |　　..:;;;;;;|.＼. （ ＼　 l. |　　..:;;;;;;|
　　　|::＼∨丿 ″..:;;;;;|　　　|::＼∨丿 ″..:;;;;;|
　　　|:::　（　( 　ﾞ　..:;;;;;|　　　|:::　（　( 　ﾞ　..:;;;;;|

http://rio2016.5ch.io/test/read.cgi/math/1781308317/229

231: １３２人目の素数さん [sage] 2026/07/15(水) 13:45:33.56 ID:SCzzBMEs

［p 進タイヒミュラー理論］
複素数体上の双曲的代数曲線とそのモジュライ空間の一意化理論としては, （ケーべ
の一意化定理, ベアス理論などを含む）タイヒミュラー理論が古典的に確立されていま
す. 一方, p 進体上の（偏極）アーベル多様体とそのモジュライ空間の一意化理論として
は, セール・テイト理論が１９６０年代に確立されています. しかしながら, p 進体上の
双曲的代数曲線とそのモジュライ空間の一意化理論は, 望月さんの研究以前には満足の
いくものがほとんどありませんでした. （マンフォード 一意化理論はありましたが, これは,
タイヒミュラー理論ではなくショットキー一意化理論の類似です.）
タイヒミュラー理論は, 通常の定式化では純に複素解析的なものであり, p 進的類似
を求めることは不可能に思われます. そこで, 望月さんは, タイヒミュラー理論の固有束
による定式化に着目し, これを足がかりにして p 進タイヒミュラー理論を構築していき
ました. その際, 技術的な核となったのは, 正標数代数多様体の上のクリスタルの理論や
p 進代数多様体の p 進ホッジ理論などです. その結果, 代数曲線とそのモジュライ空間
の望ましい p 進一意化理論が完成し, 曲線のモジュライ空間上の標準フロベニウス持ち
上げと標準座標, 曲線の標準持ち上げ, 曲線の数論的基本群の PGL 2
への標準表現, など斬新かつ基本的な対象たちが続続と発見されました. これらの結果は,
約２００ページの大論文 [1] と５００ページ超の大著 [2] にまとめられました.
p 進タイヒミュラー理論の応用としては, 望月さん自身によって, 曲線のモジュライ
空間の既約性の別証明や, 遠アーベル幾何（絶対 p 進グロタンディーク予想）への応用
などが得られています. また, 望月さんのこの斬新な理論は, F. Oort, B. Moonen ら曲
線・アーベル多様体のモジュライの数論幾何の研究者, A. Ogus, B. Osserman ら正標数
代数幾何の研究者, F. Voloch ら代数幾何的符号理論の研究者など, さまざまな分野の研
究者の注目を集めています.
上記の著書の題名が物語るように, 望月さんの手によって p 進タイヒミュラー理論の
基礎は確立されました。

http://rio2016.5ch.io/test/read.cgi/math/1781308317/231

242: １３２人目の素数さん [] 2026/07/17(金) 20:06:06.33 ID:zMIRi+X7

ID:13yLpBZq さん、労作ありがとう 転載しておきますね
https://itest.5ch.io/rio2016/test/read.cgi/math/1774529018/884-891
<Interuniversal geometry とABC 予想60>より
0884 １３２人目の素数さん 2026/07/08(水) 02:19:41.99
Claude Opus4.8とFable5使ってIUTを1から地道に検証するプロジェクトを個人的にこの一ヶ月やってみたがFable5の言い分は以下だった
IUT理解者に対する要請部分のみを書く

4. 要請
以下のいずれか一つをご教示いただきたい:

(A) 箇所の特定: (P) が(定義的措定ではなく)導出されている箇所 —— 論文・節・命題/Remark 番号 —— の特定。 すなわち、ラベル配置「テータ値 q^{j²} が j 成分に置かれる」から 受信側測度の主張「その可能な像の包が深さ ⌊j²·ord(q)−d−a⌋−b の領域に含まれ、 その体積が同じ正規化で q-標対象と比較可能である」への移行が遂行されている箇所。
(B) 機構の提示: (A) が「複数箇所の組合せから従う」場合、その組合せの明示 —— 各ステップが (i) 特定された構造の間の同型、(ii) 特定された正規化での体積計算、 (iii) 特定された領域の包含、のいずれかである形の命題列+証明の概略。
(C) 同値な別形: 実曲線(の無限族)に対する評価 L ≥ (l(l+1)/12 − 1)·|log(q)| の導出 (F3 により (P) の一様供給とこれは同値である)。

5. 予備的注記(想定される応答について)
以下の応答は既に形式化・検証済みであり、(P) の導出には至らないことを予め注記する:

「多輻的表示の定義から直ちに従う」 —— 定義はラベルを与える。要請しているのは ラベル→測度の移行であり、その移行こそが (P) である。
「同一のプライム・ストリップが両方の intertwining を同時に担う(∧ の妥当性)」 ([EssLgc] の AND 論法)—— 弱化構造(O^×μ + 抽象位相群)のレベルでの ∧ の成立は 検証済みで、我々もこれを認める。しかしそのレベルでは体積が定義されず、 ∧ から従う体積命題は containment(下界側)のみである。
「単数の共通性が体積比較を可能にする」([IUTchII] Rem 4.10.3 (i))—— 形式化済み。単数部の輸送は等長であり、従う深さは ord(q) である(F2)。
「(Ind3) 上半両立性が包を強制する」 —— 形式化済み。(Ind3) は包を拡大する 方向に働き、上界を悪化させる。拡大を抑える台帳が Prop 1.1–1.4 であり、 その大きさは |log(q)| に依存しない(F3)。

6. 検証のコミットメント
(A)(B)(C) のいずれかが供給されれば、我々はそれを既存の形式化 (受け口となる構造は実装済み)に接続して機械検証することを約束する。
導出が成立すれば、検証結果は「Thm 3.11 ⟹ Cor 3.12 の連鎖は結論の独立な導出を含む」 —— すなわち望月理論側の確定 —— に翻り、その旨を同じ厳密さで記録する。
本要請は反駁ではなく、係争を機械検証可能な一点に絞り込んだ上での、 その一点についての情報提供の依頼である。

つづく

http://rio2016.5ch.io/test/read.cgi/math/1781308317/242

243: １３２人目の素数さん [] 2026/07/17(金) 20:06:51.79 ID:zMIRi+X7

つづき

なお、6で我々は(A)(B)(C)のいずれかが供給されればLEANの形式化と接続して機械検証すると言ってるが、俺は中身はほとんど理解してないので、これは我々と言うよりは純粋にFable5の言い分となる
もし7月17日にLANAプロジェクトでGithubが公開されなければ公開するかもしれんが、Fable5が利用クレジットでの利用じゃなく、再度月額プランのみで使えるようになったらでないとFable5でやるつもりはない他のモデルではやるかもしれん

ちなみに3.11までは特に問題なくLEAN化は成功して、3.11を認めた上でのCor3.12の証明も機械検証は難なく通った
問題はそれがトートロジー的閉ループを構築していることに帰着すること
しかしそれは望月が論文内で言及していて問題ないとする部分でもある

4要請の前の0〜3は以下
0. 一行要旨
IUT 4論文の主張のうち、機械検証(Lean 4)で正しさを確認できた部分と確認できなかった部分の境界が、 [IUTchIV] Thm 1.10 証明 Step (v) の一入力 —— λ := ord(q^{j²}) を受信側正規化の体積計算に適用してよいこと —— に正確に一致した。この入力の導出(定義的措定ではなく)の所在をご教示いただきたい。

1. 背景: 何を検証済みで、何を疑っていないか
我々は IUT 4論文([IUTchI–IV])+星裕一郎『宇宙際 Teichmüller 理論入門』を底本に、 Lean 4 + Mathlib による形式化(67モジュール、sorry/axiom 0、標準公理のみ)を行った。 以下は証明として再構成でき、正しさを確認した部分である(疑義はない):

[IUTchIV] Prop 1.1–1.4 の台帳計算: different の上界(不分岐 d=0、順分岐 d=e−1、 暴分岐 d ≤ e−1+e·v_p(e))、対数殻の半径定数 a, b、殻の包含と体積公式。 (順分岐上界など、Mathlib に存在しない定量評価は新規に証明した。)
p 進 exp/log の解析理論: 収束・加法性・ノルム保存(等長性)・全単射性 (Newton 反復による全射性)。すなわち log-link の単数部 (O^×μ) は体積を保存する —— [IUTchIII] Prop 3.9 の体積両立性と整合する。
Kummer 理論の機構: 両立的巾根系・Kummer 類のコサイクル律・well-definedness、 円分剛性関連の非自明性、「1 の巾根 ↦ 0(不定性なし)」条項([IUTchIII] Thm 3.11 (ii))。
containment 側の導出([IUTchIII] Cor 3.12 証明 Step (xi-d)–(xi-f)): q-標対象の像が可能な像の包に含まれることから −|log(q)| ≤ −|log(Θ)| が 「follows formally」に従うこと。ℝ の同一視を用いずに検証した。
[IUTchIV] Thm 1.10 の最終算術: C_Θ ≥ −1 から高さ不等式への初等的演繹、 および Thm 1.10 → Cor 2.2 → Szpiro/abc 型不等式の連鎖。

つづく

http://rio2016.5ch.io/test/read.cgi/math/1781308317/243

245: １３２人目の素数さん [] 2026/07/17(金) 20:09:43.86 ID:zMIRi+X7

つづき

3. 形式的に確定している事実
(F1) Step (v) の本文が (P) の根拠として引用するのは [IUTchIII] Thm 3.11 (i)(a)(b), (ii) の定義である。多輻的表示の定義はテータ値 q^{j²} をラベル j に配置するが、 配置(ラベル)と受信側測度(体積)は論理的に別の水準にある
(F2) 当該箇所で利用可能な機構 —— 単数部の共通性([IUTchII] Rem 4.10.3 (i): "this coricity of the units will allow us to compare volumes on either side of the Θ×μ-links")、Kummer 同型、log-link、(Ind1)(Ind2)の等長性、(Ind3)の上半両立性 —— は、p 進 exp/log の等長性の帰結として**全て体積保存(lossless)**である。 これらのみから従う輸送像の深さは各レベルで ord(q) であり、j²·ord(q) ではない。 なお値群部分については [IUTchII] Rem 4.10.3 (ii) 自身が "the 'value group' portion ... is by no means preserved by the Θ×μ-links!" と述べ、 その「volume distortion の計算」を "the ultimate goal of the present series of papers" と位置づけている —— すなわち入力機構ではなく出力目標である
(F3) このとき次が形式的定理である: 分岐台帳を L(≥ 0)として、 (P) 型の体積評価が containment と両立して成立し得ることは、 L ≥ (l(l+1)/12 − 1)·|log(q)|(受信側正規化)と同値。 Prop 1.1–1.4 の台帳は O(log-different + log-conductor + l·log(e*·l)) であり |log(q)| に依存しないから、実曲線の族(高さ非有界)に対して (P) を一様に供給することは、 導かれるべき高さ不等式を供給することと論理的に同値である
(F4) [IUTchIV] Rem 1.10.1 は、Thm 1.10 の計算(主要項)が [HASurI] Thm A の Hodge–Arakelov 計算と本質的に同一で「2000 年頃には著者に知られていた」こと、 問題は「その計算を遂行できる枠組みの構築」であったことを明言している。 我々の検証はこれと整合する: 計算は正しい(検証済み)。未検証なのは、 枠組みがその計算の (P) としての読みを正当化するという主張の導出である
(引用終り)
以上

http://rio2016.5ch.io/test/read.cgi/math/1781308317/245

246: １３２人目の素数さん [] 2026/07/17(金) 20:22:24.71 ID:zMIRi+X7

「LANAプロジェクト」中間発表会 動画 「LANAプロジェクト」中間発表会
結論は、7月17日時点では、未決着（灰色）
キラン・ケドラヤ氏説明は、コンピューター検証 は 未達成だが、IUTがダメということも言えない
ということだったな

（下記の YouTube（日本語チャンネル））
https://youtu.be/g0QLL8iYECY?t=590
UT理論のコンピューター検証に関する「LANAプロジェクト」中間発表会
ZEN大学
1,504回視聴  7 時間前にライブ配信
ZEN大学「ZMC（ZEN Mathematic Center;ZEN数学センター）」は2026年7月17日（金）、IUT（宇宙際タイヒミューラー）理論のコンピュータ検証に関する「LANAプロジェクト」の中間発表会「LANA Project Interim Report 2026」を行います。
本発表会の模様をライブ配信いたします。

LANAプロジェクトはZEN大学（日本）、ユトレヒト大学（オランダ）、アルバータ大学（カナダ）を中心とする国際共同研究プロジェクトであり、数論幾何学の重要分野である遠アーベル幾何学の形式化と、京都大学数理解析研究所の望月新一教授が提唱したIUT理論の検証を主な目的としています。

【登壇者】
若山 正人（ZEN大学 学長）
加藤文元（ZEN大学教授・ZMC所長、LANAプロジェクト リーダー）
ヨハン・コメリン/Johan Commelin（ユトレヒト大学助教）
キラン・ケドラヤ/Kiran Kedlaya（カリフォルニア大学サンディエゴ校 教授）
アダム・トパーズ/Adam Topaz（アルバータ大学 准教授）

❙ ZMC（ZEN Mathematics Center; ZEN数学センター）とは
ZMCは、数論幾何学を中心とした現代数学や、コンピューター言語を用いた現代数学の形式化（formalization）の推進と発展を目指して設立された国際研究所です。
ZMCホームページ▶https://zen.ac.jp/zmc

https://zen.ac.jp/news/zmc0717
ZEN大学 2026/07/03
プレスリリース
IUT理論のコンピューター検証に関する 「LANAプロジェクト」
中間発表会を7月17日（金）に開催
YouTube、ニコニコ生放送にてライブ配信
番組配信：
YouTube　（日本語チャンネル）：https://www.youtube.com/live/g0QLL8iYECY
YouTube　（英語チャンネル）：　https://www.youtube.com/live/KADN5NHmIfw
ニコニコ生放送（日本語のみ）：　https://live.nicovideo.jp/watch/lv350854170

http://rio2016.5ch.io/test/read.cgi/math/1781308317/246

252: １３２人目の素数さん [] 2026/07/17(金) 21:35:29.08 ID:zMIRi+X7

>>251 補足
下記の 「ワイルズによるフェルマーの最終定理の証明」が、参考になる
ギャップがあったが、
ワイルズ氏はそれを埋めることができた

今回も同様と思う。ギャップがある。ギャップを埋められるかどうか？
一方、ショルツの指摘は真逆で、全然ダメで 箸にも棒にもかからないのだと
ケドラヤは、ショルツの見方を否定する

(参考)
https://ja.wikipedia.org/wiki/%E3%83%AF%E3%82%A4%E3%83%AB%E3%82%BA%E3%81%AB%E3%82%88%E3%82%8B%E3%83%95%E3%82%A7%E3%83%AB%E3%83%9E%E3%83%BC%E3%81%AE%E6%9C%80%E7%B5%82%E5%AE%9A%E7%90%86%E3%81%AE%E8%A8%BC%E6%98%8E
ワイルズによるフェルマーの最終定理の証明
証明の発表とその後
ニック・カッツがワイルズの論文の査読を行うレフェリーの一人として指名された。カッツはレビューにおいて、ワイルズに証明に関する様々な質問をしたが、そのうちにワイルズ自身も認めるギャップが証明に含まれることがわかった。証明の重要な箇所（ある種の群の位数に上限を与える部分）の誤りであり、コリヴァキアン＝フラッハ法を拡張するのに使用したオイラー系（英語版）が不完全だったというものだった。

ただし、この誤りによってワイルズの仕事が全く役に立たないものになったわけではなかった。ワイルズの証明のそれぞれの部分は単体でも意義深く革新的なものであり、証明の過程で多くの発展や新たなテクニックが見出されていたためである。この誤りに影響されたのは一箇所のみであった[9]:289, 296–297。しかしながら、この一箇所が（誤りによって）証明されないのであれば、フェルマーの最終定理の証明も成されない。

ワイルズはギャップを取り除くのにほとんど1年を費やした。当初は自身で訂正を試みたが、のちにかつての指導学生であるリチャード・テイラーの協力を仰ぐこととなった。1993年の終わりまでに、厳しい視線が注がれるなかでワイルズの証明が失敗したという噂が広がったが、どの程度深刻なのかに関しては知られていなかった

ワイルズによれば、1994年9月19日の朝、彼はほとんど誤りの訂正を諦める寸前で、証明に失敗したことを認める瀬戸際におり、他の数学者が証明を発展させ、誤りを探すことができるように証明の詳細を発表しようとしていた。彼は証明がなぜ不完全だったのかを理解するための最後の確認をしていたが、不意に、コリヴァキアン＝フラッハ法の適用の際に問題となっている部分そのものが（コリヴァキアン＝フラッハ法のアプローチから得た経験を援用することで）岩澤理論の適用を可能にすることに気がついた。それぞれのアプローチは単体では不適切だが、両者のアプローチを組み合わせ、双方のアプローチのツールを使用することでギャップを取り除き、（ワイルズが最初に出した論文では証明が与えられていなかった）すべての場合に有効な類数公式(Class Number Formula, CNF)を与えた。[13]。

http://rio2016.5ch.io/test/read.cgi/math/1781308317/252

262: １３２人目の素数さん [] 2026/07/18(土) 09:06:58.95 ID:HVwj1DT/

>>246
議論のネタ追加

＜ケドラヤの発表＞
https://youtu.be/g0QLL8iYECY?t=2990
UT理論のコンピューター検証に関する「LANAプロジェクト」中間発表会
ZEN大学
1,504回視聴 7 時間前にライブ配信
ZEN大学「ZMC（ZEN Mathematic Center;ZEN数学センター）」は2026年7月17日（金）、IUT（宇宙際タイヒミューラー）理論のコンピュータ検証に関する「LANAプロジェクト」の中間発表会「LANA Project Interim Report 2026」を行います。
本発表会の模様をライブ配信

＜文字起こし＞
49:50はい、加藤先生、ありがとうございました。続いてキランケドラヤ先生お願いいたします。
＜ケドラヤ＞
50:08え、2018年ピーターショルツとジャコブ スティクスは、議論を理解しようとする目的で京都の望月氏を訪問しました。
ショルツとジャコブ スティクスは
50:21IUTはABC予想を証明していないとし 、さらに証明することもできないという 結論を出しました。彼はその証見を次の
50:29原稿の形で、え、マニュスクリプトの形で報告を しました。で、この、え、結果は所見は
50:37IUTの位置付けは既でに決着済みの問題で あるという合意に、え、したわけですが、
50:44これに対してプロジェクトの立場は現時点で はIUTに基づくABC予想の証明を持っ
50:50ていないが 一方で証明の詳細 すなわち教授が述べたようなとしてEタータを証明するために必要な詳細 がある可能性があり得 ということを言っています。
51:13このこれらの分析の根拠はショルツ スティクス 分析の根拠はいずれも内部の
51:21議論の細かい部分を考慮せずにIUTの論理構造 をモデル化することから始まります。
51:28スティクスの場合はこの分析は次のような 一次元ベクトル空間の図式を生じさせます。この下に書いてある図式ですね。
51:37しかしこの式は、え、図式は可換で はありません。2つの経路は
51:45 2つのパスを左上から、え、右下まで行きますと、この2つの経路を逆向きに
51:55逆時計回りをしても、え、可換ではありません。
52:07これによって障害となるわけですね。
52:15で、ショルツスティクスはこの図式を用いて IUTへのIUT理論への障害を特定
52:22しようとしました。ただこれが難しいのは 彼が
52:28彼の分析は不定について意味のある技術を与えるほど精密ではないからです。
52:37え、望月の、そしてこの ショルツスティクスの引用文をこれから
52:44申し上げます。略
52:50と主張した。この主張が意味するのはその ぼかしが少なくとも 略でなければならずそのためこうして得
52:59られる不等式は役に立たないということのように思われると起述したわけです。

つづく

http://rio2016.5ch.io/test/read.cgi/math/1781308317/262

263: １３２人目の素数さん [] 2026/07/18(土) 09:07:36.37 ID:HVwj1DT/

つづき

53:05しかしそれに対して私は申し上げたいことは不定性が実数に直接作用することを、え 、示唆していますが、これは望月の方法を
53:14正確に表したものではないんです。この分析では不定性はボリュームコンテナー
53:22の部分集合に作用するということであり、 従ってその実数上への影響を直接 トラッキングすることはできません。
53:31実数のサブセットに対する影響は このIUTによる
53:41ABC予想にいかなるの証明も、略 に押し込めることができるとショルツ
53:49スティクスは仮定してるわけです。その分析についてこの形として
53:57この実数が略 トッパーズ教授の
54:06スライドでありましたようにこの実数中で 図を用いて先ほどのスライドの
54:13実数の証明であるわけですが、従がって これはこの想定として、え、不等であると いうことは、略
54:21詳細の分析は、え、Qパイロット オブジェクト、え、ベツパイロット オブジェクトが対して2つの変化異なる 生じることを示しています。一方我々では
54:31特にこの不等式 として、え、この 3.12に関しまして同じキューパット
54:39オブジェクトからです。そのうちの1つが 直接な計算演算、すなわちQ ホルモティフィックストラクチャーを
54:46用いる計算です。もう1つは、え、この リンクを経由する間接的な演算であります 。
54:56この体積をボリュームを共通のコンテナーに 入れるためにはショルツスティクスが描いたもので はない図式の可換性が必要です。
55:06しかしその図式は、え、イーター、または イタアナブのいずれかとして様々に解釈さ れなければならない矢印を含んでいます。
55:19その 結果、え、その不等になるかどうかということで、望月氏の、え、言葉で言えばトロジカルな理由で成り立たされているこの式であるのです。これがさらなる進展の鍵となります。
55:35サンキュー。それでは発表は以上となります。え、それではここから会場にお越しの皆様からご質問をお受けしたいと思っております
(引用終り)
以上

http://rio2016.5ch.io/test/read.cgi/math/1781308317/263

264: １３２人目の素数さん [] 2026/07/18(土) 09:30:31.61 ID:HVwj1DT/

>>262-263 補足

プロジェクトメンバーの
ヨハン・コメリン/Johan Commelin（ユトレヒト大学助教）
キラン・ケドラヤ/Kiran Kedlaya（カリフォルニア大学サンディエゴ校 教授）
アダム・トパーズ/Adam Topaz（アルバータ大学 准教授）

3名の立場は
１）ショルツ スティクス 分析は、望月氏の3.12を全否定しているが
　しかし、その分析は不十分
２）望月氏の現時点のIUT論文から 形式的なLeanコードに 落とすことはできなかったが
　何かを補えば 3.12を Leanコードに 落とすことが出来る可能性は残っている
ということでしょう

私見だが
あたかも、下記 ガウスの代数学の基本定理証明で、ジョルダン曲線定理を自明として使ったが
まあ、1799年当時としては それは 多くの人に自明と思われたのだが
後年 ジョルダン曲線定理は 要証明だとされて
「ガウスの代数学の基本定理証明は、ちょっと滑っていたね」という結論になった

望月IUTが、どういうことを”自明”としていたのか？
それはともかく
玉川安騎男氏など 多くのIUT支持派も 無意識に”自明”で流していた部分が
あったのではないか？
それが、Leanコードに落とすときに 引っかかったという風に理解しました

なので、あたかも
ガウスの代数学の基本定理証明のジョルダン曲線定理相当部分を
きちんと定式化して 証明を与えられるか？
そこがポイントでしょうね

面白くなってきました
頑張れ、モチヅキ！！

(参考)
https://ja.wikipedia.org/wiki/%E4%BB%A3%E6%95%B0%E5%AD%A6%E3%81%AE%E5%9F%BA%E6%9C%AC%E5%AE%9A%E7%90%86
代数学の基本定理
歴史
1799年にカール・フリードリヒ・ガウスが学位論文でそれまでの証明の不備を指摘し最初の証明を与えた（ただし、現在ではガウスの最初の証明も完全ではなかったことが分かっている[注 1]
注釈
1. ガウスの最初の証明は幾何学的な前提としてジョルダン曲線定理が暗黙で使われており、後年の観点からは不備がある。

http://rio2016.5ch.io/test/read.cgi/math/1781308317/264

上下前次 1-新書関写板覧索設栞歴

あと 14 ﾚｽあります
ｽﾚ情報赤ﾚｽ抽出画像ﾚｽ抽出歴の未読ｽﾚ AAｻﾑﾈｲﾙ

ぬこの手ぬこTOP 0.024s