Interuniversal geometry とABC 予想61 


>>886
説明できないおっさんの末路だせえw

>>887
そうか

>>887
どうしてほしいと思ってるのかな

>>889
とっとと退場
税金使うな私費でやれ

>>885
とりまきに囲まれた裸の王様、、

ナビエストークスもおちたか

AIがミレニアム懸賞問題の一つ
ナビエストークス問題を解いた
話題ですか

-

AI Has Solved One of Math’s $1 Million Millennium Prize Problems

quanta magazine
2026年9月8日

https://www.quantamagazine.org/ai-has-solved-one-of-maths-1-million-millennium-prize-problems-20260908/ppl

ナビエストークスのやつは性質調べるだけって
言ったらなんだけど
勘とHPCでいけそうな気もするが
LEANのところはLLM強いんだろうな
数日で結果出せる

一方、、

はよAIにknotの完全分類やって欲しいね

何を持って完全分類と呼ぶかになる
もう同値性の判定アルゴリズム自体はある
そこから先なんか面白い分類定理(有限単純群のときみたいな)こんなやつの全体で尽くされるのようなリストが作りうるかどうか
双曲型やザイフエルト型のリストアップくらいはできそうだけど
もう同値生判定アルゴリズムができた時点であんまり発展性は感じない

>>894
AIって名目なら金、計算資源が出せるってのは大きい

>>894
物理でも数学でもないパラダイムシフト
した望月IUTならハレーションおこして
カーネルを通過するかもしれませんね、

>>898

追加
>>231

IUT論文について共同通信記者からケドラヤへ質問。
PRIMSの受理と査読について
(ケドラヤはlean形式化もIUTもど素人).

1時間11分頃から

https://m.youtube.com/watch?v=2jgBBw6XjQ4&ra=m

　

>>894
君はLANAって全くわかってないよね。

age

>>901
え？知ってるけどw
IUTおじさんクソレス入れんなよゴミ

類体論の解析学を使う証明はLEANを通せるのかな？

楽勝です

kevin buzzardによる局所的.大域的類体論のleanによる形式化プロジェクトは、現時点で類体論が部分的に形式化された。

・主要な主定理（高木・アルティンの相互法則など）をすべて穴「公理化」がなく完全に証明しきるには至っていない、mathlibも同様だ。

・leanによる形式化は L関数など解析的方法を迂回しより容易な代数的方法に置き換えることも必要だろう

フェルマー定理のlean証明はできたらしいから類体論の証明体系も完成したと思ってたが違うのか

>フェルマー定理のlean証明はできたらしい

フェルマーの最終定理は証明された。
leanにより完全に形式化されたのか？
カーネルを通過したからOKになった
のか？

>>909
自分で調べればいいじゃん
https://github.com/anthropics/fermats-last-theorem

leanによる類体論の形式化についてだが、

FLTの証明でleanによる形式化に
必要な類体論の部分に限り　形式化したのでありscholzeの懸念の視点
からも検証が必要だ

>>910
あなたは調べたの？

>>912
調べてないよ。

・scholzeの懸念
　>>40

・Xena
https://xenaproject.wordpress.com/2026/09/04/flt-anthropic-has-beaten-me-to-it/

IUTキチガイ、ランダムウォークスレ作ってクソ漏らすの巻

https://youtu.be/4JPLTOYoqXI?si=wo1Z_joispUSOCrb

AIって問題は解けるけど新しい理論とか手法は作れるんけ

重力理論と装置をつくってみた(螺旋重力 Spiral gravity)
https://rio2016.5ch.io/test/read.cgi/sci/1745635184/


IUTと双璧のキチガイ朝鮮人研究

ほらな
北朝鮮在日だろ？

「永遠の敵対はない」笹川陽平・日本財団名誉会長がロシア訪問　日露関係改善に意欲 　(産経) [少考さん★]
https://asahi.5ch.io/test/read.cgi/newsplus/1789864420/

>>914

lean3から入れ子構造機能など
を加えたlean4は健全性の証明が
未証明らしい。


➖
・コラッツ予想の偽.反証の証明

https://gigazine.net/news/20260803-collatz-lean-kernel-bug/

・『Lean で証明できた』は何を保証するのか？ 〜 Lean の無矛盾性と信頼の根拠 〜

https://arxiv.org/html/2403.14064v2

>>920
追加

https://qiita.com/kyamaz/items/7b38e5977dc97747d2d9

伊藤穰一/笹川/マクスウェル/エプスタインラインな
ちなみにイスラエル建国当時の国民の半分がソ連人

「永遠の敵対はない」笹川陽平・日本財団名誉会長がロシア訪問　日露関係改善に意欲 　(産経) [少考さん★]
https://asahi.5ch.io/test/read.cgi/newsplus/1789864420/



で、こいつらと仲良いっていうか一心同体なのが
旧満州北朝鮮在日わんごおおおおおおおw

lean3から入れ子構造機能など
を加えたlean4は健全性の証明が
未証明らしい。

健全性の証明が未証明ってどこにそんなことかいてあるん？

>>921

>この結果は Lean3 のものです。
Lean4 では型理論が拡張されており（入れ子の帰納型、構造体に対する 規則など） Carneiro 自身が後の論文で「2019年の健全性証明はもはや直接には適用できない」と述べています

ほんまやね。まぁそのうち証明されるやろけど。たぶん純理論的には問題ない。一部残ってるかもしれないヒューマンエラーが洗い出されれば安心して使えるでしょ。Lean の基礎理論(数学部分)とコーディング部分の正当性を Lean に検証させるプロジェクトも実行中らしいし。それが通ったらもう信頼性はほぼ完ぺきになるやろな。

最近は話題にならなくなった

>>926
7/17に中間発表だから年明けに最終発表がある
スケジュール考えると数学的結論は10月末頃には出てないといけないだろう
中間発表で結論は出てるから望月の同意を得られるかどうかしか争点はないが

そもLeanに翻訳するのが難しいと言われるといつ終われるのか分からんな


【ReHacQ生配信】AIで数学を証明!?IUT理論は正しいのか【高橋弘樹vs川上量生vs野村泰紀vs加藤文元】
https://www.youtube.com/live/b6JlM_nrM3M


━━ LANAプロジェクト（IUT理論の検証プロジェクト）の進捗状況については、1時間03分30秒頃から語られています。加藤先生と川上氏が、プロジェクトの中間発表の内容や、現在の到達点について詳しく説明しています。

•判断の保留: 現時点では理論が正しいか間違っているかを断定する段階には至っておらず、引き続き検証が必要な状態であること（1:03:32-1:04:10）。
•言語化の壁: コンピュータ言語（Lean）へ翻訳するための前提となる人間側の理解において、まだ解明すべき難所があること（1:04:11-1:07:25）。


━━ 遠アーベル幾何学の内容をコンピュータ言語である Lean に落とし込むプロジェクトについての話は、1時間36分49秒頃から始まります。

このパートでは、IUT理論の根幹をなす遠アーベル幾何学を計算機上で扱うことの難しさと、なぜそれが重要なのかについて以下の点が語られています：

• IUT理論と計算機科学の接点: IUT理論自体は非常に難解でキャッチーな話題ですが、その土台となる遠アーベル幾何学を Lean に落とし込むこと自体が、数学研究における新しい手法として重要であると説明されています (1:36:51-1:37:04)。
• プロジェクトの意義: IUT理論を検証する過程で、この基盤となる理論をコード化することは、現代数学の新しい検証手法としての大きな実績になるという議論がなされています (1:37:05-1:37:14)。

今までは権威で逃げ続けてきたけど
AIとLeanがたいていの数学者より信頼できるようになった今はもう通用しないだろうな
尊師は定年までゴネ続けるんだろうけど
付いていった任期付きの取り巻きたちの敗残軍は残りの人生どうすんのかなw

>>929
笹川朝鮮財団に媚びて生きていくしかないんじゃねーのか
惨めだわな

>>925

>まぁそのうち証明されるやろけど。たぶん純理論的には問題ない

健全性が証明されていないなら
数学の証明として不完全でしょ。
L ANAはzen大学の話題ほしさと
scholzeたたきの茶番劇ですね。
leanのコンパイラカーネルを無理やり通過したからOKなんだろうなあ、

「LEANが証明したLEANの正しさ」ということを真面目に信じてよいものであるかどうか。
あるところに嘘つきがいて「私は正直者ですよ」というのとあまりかわらないことになるのでは？

FLTのleanによる定理証明支援系
では元々確立した自然言語の
Wiles–Taylorの証明がある。

一方、
望月新一独特のIUT語による
「 abcの証明」はzen大学を含むとりまきと日本しか通用していない。実際
IUTはICM2026のlectures
にもなかった。

Leanが通らなかった以上どれだけショルツの揚げ足取りしようが望月サイドの完全敗北だろ

あほなんじゃないのかな？健全性に疑義がのこるってのは「正しくないのに正しいって判定される可能性がある」って意味なんだけど？あほなん？

Lean以前に証明を誰も追えないのが望月さんの証明
形式化以前に誰も納得してない
正しいと言ってるほんのごく少数の人間も他人に説明出来ない
星さんの苦渋のコメントを読んでみろ
納得出来てないだろw
Lean関係ない
全く関係ない

>>928
>• プロジェクトの意義: IUT理論を検証する過程で、この基盤となる理論をコード化することは、現代数学の新しい検証手法としての大きな実績になるという議論がなされています (1:37:05-1:37:14)。

研究者のキャリア上重要な業績になるようなことじゃない
他の事やるよ
まあ望月の証明が正しければ話は少し違うんだが

もしもIUTを仮定すればRHが導けたら面白いだろうね。

iutを仮定したらなんでも解けるんじゃね？

・(>920) (>921)-(>>924)

『Lean で証明できた』は何を保証するのか？ 〜 Lean の無矛盾性と信頼の根拠 〜

・
Postmortem for Kernel Soundness Bug #14576

> Verification
Mario Carneiro's lean4lean is a Lean formalization of Lean's type theory together with a proof that the kernel implements it.
The work is ongoing, the proof of consistency does not cover inductive types yet, and the
to-be-verified implementation suffered from the same bug as the official kernel.
The bug would have been found when attempting to conclude the verification of this part.

https://leodemoura.github.io/blog/2026-8-1-postmortem-for-kernel-soundness-bug-14576/

まだいってるよ。lean 3 から lean 4 への拡張って let rec の追加、structure η と浮動小数点計算のなんからしい。そして lean 4 があぶないならたとえそれでOKでも Lean 3 では通らない可能性があるにはある。しかしその場合 let rec を全部はがして top level 再起に書き換えて structure ηの証明を書き加えたらそのまま lean 3 で通せる。そして lean 4 でダメなやつは lean 3 でもダメ

てかそもそも lean 4 がまだ信頼でいないなら lean 3 でかけばいいやろ

>>942
leanのせいにしたいんだろ

正直もうabcとか興味ない