探検


Interuniversal geometry とABC 予想61 


1132人目の素数さん
垢版 |
2026/07/12(日) 21:44:34.29ID:c76i8A5Q

未だにcontroversialなIU幾何やABC予想に関する会話のサロンとして使って下さい。

荒らしはご遠慮願います。
2026/07/30(木) 23:12:29.79ID:RwAHr5Hk
>>651
誹謗中傷はIUT側からしか出てきてないが?
2026/07/31(金) 09:52:35.03ID:OfhfHjkl
コミュニケーション(失笑)の具体例出せないIUT擁護派www
2026/07/31(金) 09:53:33.78ID:OfhfHjkl
じゃあ日記形式で我慢してやるから出せよ
コミュニケーションしてんだろ?
してねーのにフカしてねーだろうな
zen大学www
655132人目の素数さん
垢版 |
2026/07/31(金) 10:13:48.44ID:r/hcKBTn
コミュニケーションツールだのライブラリの整備だの
要するにIUTで何の成果も出せないことのゴマカシじゃん
がんばりました。何の成果も出せませんでした。じゃかっこ付かんけんね
2026/07/31(金) 12:40:32.57ID:OfhfHjkl
ニコニコ、有料会員が8月から再値上げ 月額790円→990円に😲 [861717324]
https://greta.5ch.io/test/read.cgi/poverty/1785385818/
657132人目の素数さん
垢版 |
2026/07/31(金) 13:25:16.81ID:zXrbsCk7
>>644

その通りですね。
AIとlean4の数学証明支援系はハッキングに脆弱でした

➖
コラッツ予想の偽証明.
・AI(LLM)がlean4の証明支援系
の核心部で、プログラミング言語などが「安全である・正しい」と保証している性質(健全性)の誤り不具合(バグ)を発見し健全性のチェックを通過した。
このバクを利用して偽から証明
作成すればなんでもありの
偽証明になる。
658132人目の素数さん
垢版 |
2026/07/31(金) 13:28:03.78ID:zXrbsCk7
p.scholzeのlean証明支援系へ感想。

14分過ぎあたりから.
https://m.youtube.com/watch?v=_gAe77G_aHw&ra=m
2026/07/31(金) 13:59:50.31ID:OfhfHjkl
>>657
>>644
バカチョン低学歴IUTワラタw
何もわかってねえ

その間違いすらわかるからいいんだよゴミ朝鮮w
間違ってすらいないゴミIUTとくらべんなゴミが
2026/07/31(金) 14:03:15.18ID:OfhfHjkl
「IUT理論は定理3.11までは誰も文句は言っていないらしいね。そこまでは大きな成果を誇れるらしい。」
👆
大嘘

「ちなみにIUT理論批判者は3.12に矛盾があるかどうは示してはいないらしいね。」
👆
大嘘

「かといって反例などで間違いを示せてもいないらしい。」
👆
大嘘


ワラタ
661132人目の素数さん
垢版 |
2026/07/31(金) 14:05:58.75ID:zXrbsCk7
>>643 の質問1はどうですか?
662132人目の素数さん
垢版 |
2026/07/31(金) 21:59:55.60ID:qyXYZ02W
>>660
てっぺんはともかく下の二つは大嘘じゃにゃあでそ
「証明がない」という事実を無視した論点そらしにゃだけ
証明責任がどこにあるかも無視しちょる

実際「3.12=望月の不等式」に反例があったら大したもんでそ
663132人目の素数さん
垢版 |
2026/07/31(金) 22:02:35.99ID:qyXYZ02W
もちろん「望月の不等式(予想)」って意味ぞな
2026/07/31(金) 23:25:32.84ID:jpxU4lR4
そもそも概念自体が形式化できてないんだから反例のだしようもない
数学の議論が始められる状態ですらない
2026/08/01(土) 01:30:23.41ID:zg7JijSf
>>662
ショルツにいきなり反例出されてんのにw
666132人目の素数さん
垢版 |
2026/08/01(土) 06:04:03.51ID:yBdpKCKL
>>664
だから、こういう定義と仮定したらうまくいかないよねって例を出したら、
なぜか間違ってる!って叩かれたでござる
2026/08/01(土) 08:14:45.10ID:rY0RPFYB
>>665
ちがうよ。ショルツいわく「ここの概念に辻褄をあわせようとするとこっちに話が合わない。だまし絵のような話」という状態だという。彼があげたのは辻褄あわない実例のひとつ。もしかしたら彼の指摘をかわしてそこの辻褄あわせるのは不可能ではないのかもしれないけど、それだとまた辻褄あわないところがでてくる。
現状そういう「反例出すことすら無理な状態」ということすら信者にはわからない
668132人目の素数さん
垢版 |
2026/08/01(土) 13:03:14.32ID:Ydz88/4E
ss論文は望月の反論やLANA中間報告書の反論で
無意味って考えてる人いるみたいだけど
学術的なリアクションがどうだったかはここ見りゃ分かるよ

https://www.semanticscholar.org/paper/Why-abc-is-still-a-conjecture-Scholze/0253b621d24779fad66e6c24312138bcc509f9da
2026/08/01(土) 15:03:40.60ID:BIPVTn2/
>>667
ニワカか
反例出されてるぞ
670132人目の素数さん
垢版 |
2026/08/01(土) 15:20:22.80ID:+iDsszXh
>>667が正しい

本当に反例があったらIUT信者だって抵抗できないわ
>>669は「反例」がなんだか引用するべし
671132人目の素数さん
垢版 |
2026/08/01(土) 16:19:19.30ID:qWBa4GHN
証明できない主張を自明だと宣う奴は数学者ではない
そんな論文をアクセプトした奴らも数学者ではない
2026/08/01(土) 17:29:41.04ID:NvwdPbqu
まぁ流石に最終報告する時にはどんな解釈のもとどんなコード組んで検証したのか発表するんだろうけどな
一年目度だっけ?
それでなんかぐちゃぐちゃ言い訳してそっ閉じするんやろな
2026/08/01(土) 17:42:04.78ID:zg7JijSf
>>670
まさかだけど
Why abc is still a conjecture
PETER SCHOLZE AND JAKOB STIX

これ読んでない(読めない)IUT擁護派低学歴在日朝鮮人がいきがってるとは、、、、
2026/08/01(土) 17:42:28.61ID:zg7JijSf
>>671
っていうか犯罪者だよな
2026/08/01(土) 17:55:01.39ID:zg7JijSf
・Scholze-Stix(2018)は
「この図式を具体的に追うと、pilot objectのconcrete normalizationを入れると矛盾(または平凡化)する」
と具体的な反例・計算の道筋を示した。
・望月側は「それは単純化の誤り」と返すが、その「誤り」を避けた具体的な計算例・修正図式を第三者に見せられていない。
・Taylor Dupuyや一部のセミナー、Kirti Joshiの試みでも、
「ここで定義が曖昧で進められない」「Θ-pilotの扱いが追えない」
で詰まる報告が繰り返されている(2025年以降も進展報告なし)。
・2026年現在も
「具体的な楕円曲線(例:y² = x³ - x + 1 とか)で、Hodge theaterを1つ構築→Θ-link→log-link→不等式の数値評価」
のような最小限のtoy exampleすら公開・検証されたものがない。
676132人目の素数さん
垢版 |
2026/08/01(土) 18:37:11.34ID:wClptXDR
ファルティングスのYouTubeの動画はどんな内容ですか?

Gerd Faltings on the 500-page ABC-conjecture proof
677132人目の素数さん
垢版 |
2026/08/01(土) 19:42:07.74ID:aC4iL968
>>676
>Gerd Faltings on the 500-page ABC-conjecture proof
Excerpt from the post Abel Prize 2026 ceremony interview.

0:00 - "If I'm at page 500, I've forgotten page 1"
0:10 - Did Mochizuki prove the ABC Conjecture?
1:00 - Faltings' official position
1:55 - "PhD students are like children..."
678132人目の素数さん
垢版 |
2026/08/01(土) 21:13:42.71ID:mPToLTXq
https://m.youtube.com/watch?v=8NpE81F0gzU&pp=iggCQAE%3D&ra=m
2026/08/01(土) 21:22:51.73ID:zg7JijSf
エプスタインと笹川&日本財団

そして、日本においては、このロバート・マクスウェルと日本船舶振興会(現在は日本財団)の創始者である笹川良一との関係に注目が集まっている。ロバート・マクスウェルと笹川良一の関係を調べると、1985年にグレイトブリテン・ササカワ財団(大英笹川財団)が設立され、ロバート・マクスウェルが理事長を務めた。この時に、当時の日本船舶振興会が約30億円を拠出したそうだ。
680132人目の素数さん
垢版 |
2026/08/01(土) 23:42:57.65ID:+iDsszXh
>>673
その文書のどこに「反例」がかいてあんの

>「反例」がなんだか引用するべし
って言われてんのに引用できないんだね
可哀そうに
2026/08/02(日) 00:06:04.86ID:Lb3Gyp67
>>680
ええええ?
メクラなの?
2026/08/02(日) 00:07:03.10ID:Lb3Gyp67
ほんとIUT擁護派はゴミしかいねーよな
っていうか数匹しかいないけど
683132人目の素数さん
垢版 |
2026/08/02(日) 00:27:55.08ID:9TAvUMoL
>>675
じゃあもう無理なんじゃない?
2026/08/02(日) 00:43:35.23ID:Lb3Gyp67
IUT擁護派は文盲やから何も読めんのや
あっても都合悪きゃ見えないメクラチョン
685132人目の素数さん
垢版 |
2026/08/02(日) 01:29:45.30ID:NYTbqL0z
「間違ってすら居ない」ってよく書いてる人いるけど
それは
既存数学で証明も反証もできないだろうちう意味よね?
全く新しい言明であって
それが既存数学と独立であろうという見立て
(その見立てが正しいかどうかも不明だけど)
でも
そうであっても一階述語論理で表現はできる筈だから
検証に乗せることができないとおかしい
686132人目の素数さん
垢版 |
2026/08/02(日) 01:33:26.88ID:NYTbqL0z
∃G,∀x∈G:P(x)∈G
が論証も反証もできないのと同じで
687132人目の素数さん
垢版 |
2026/08/02(日) 08:13:10.81ID:FLhHZHET
>>84
>・Taylor Dupuyや一部のセミナー、Kirti Joshiの試みでも、
>「ここで定義が曖昧で進められない」「Θ-pilotの扱いが追えない」
>で詰まる報告が繰り返されている(2025年以降も進展報告なし)。
ちう意味じゃね?
688132人目の素数さん
垢版 |
2026/08/02(日) 08:24:01.13ID:NYTbqL0z
>>687
それなら
間違ってる
んじゃね?
689132人目の素数さん
垢版 |
2026/08/02(日) 08:27:25.19ID:FLhHZHET
定義が曖昧というのは正しいか間違いかを論ずる以前じゃね?
690132人目の素数さん
垢版 |
2026/08/02(日) 08:34:55.93ID:NYTbqL0z
概念が正しく定義されてないならそら間違いだろうよ
691132人目の素数さん
垢版 |
2026/08/02(日) 08:53:34.17ID:FLhHZHET
なぜ?
692132人目の素数さん
垢版 |
2026/08/02(日) 09:11:34.53ID:NYTbqL0z
>>691
定義がないから
693132人目の素数さん
垢版 |
2026/08/02(日) 09:21:31.66ID:NYTbqL0z
俺はF1もモチーフも胡散臭く感じてるけど
スローガンとして?持つのは妨げられない
しかし定義も無いモノを使って何かを論じるのは
間違いジャネ?
694132人目の素数さん
垢版 |
2026/08/02(日) 09:27:31.86ID:xziEUhKp
>「間違ってすら居ない」ってよく書いてる人いるけど
>それは
>既存数学で証明も反証もできないだろうちう意味よね?

違う
「証明を成していない」って意味
もっとはっきり言えば
「同時代の専門家が認める水準の証明を成していない」
って意味

たとえばだけど、神様が目の前に現れて
「リーマン予想は正しい、証明は自明」
って言ったら、これは間違ってる?
証明の詳細を聞き返しても、
「自分と同様の専門知識を身に着ければわかる」
って言われるの
それならLeanコードをくださいっていうのを
今やってるところ

>>693 その通り
695132人目の素数さん
垢版 |
2026/08/02(日) 09:41:51.03ID:FLhHZHET
「君はバカである」はどうならバカかが未定義だから正しいとも間違いとも言えないのでは? 間違ってすらいないとしか言えなくね?

>定義も無いモノを使って何かを論じるのは間違いジャネ?
ん? 君は行為の正誤を述べてるの? ならまず行為の正誤の定義をしないと
696132人目の素数さん
垢版 |
2026/08/02(日) 09:57:38.28ID:FLhHZHET
概念が未定義で命題とされるものが実は命題になってなければ当然証明も反証もできないが、
ある理論と独立な命題もやはりそうだから、それらは区別すべきだよ。
>既存数学で証明も反証もできないだろうちう意味よね?
では区別できない。
697132人目の素数さん
垢版 |
2026/08/02(日) 10:07:27.54ID:FLhHZHET
例えば選択公理はZFで証明も反証もできないが、IUTのように「間違ってすらいない」と評されることは無いだろう
698132人目の素数さん
垢版 |
2026/08/02(日) 10:33:51.69ID:NYTbqL0z
>>697
IUTを「間違ってすらいない」と書いているのがその意味
つまり
CはZFでは証明も反証もできないだろうちう意味だと思ったので>>685,686と書いたけど
そうではなくて
「定義がなされていない」ちう意味なら
そりゃ「間違ってすらいない」でなくて「間違ってる」んじゃないかな
699132人目の素数さん
垢版 |
2026/08/02(日) 10:43:38.74ID:NYTbqL0z
まあいいや
>>685,686という意味で無いってことが分かったからいいや
700132人目の素数さん
垢版 |
2026/08/02(日) 10:55:36.54ID:xziEUhKp
ID:FLhHZHETの言う通りですが
とりあえず分かったようでなによりです

『定義が曖昧』『証明がない』ということは
数学的な真偽を判定する材料がないということ
だから「間違いですらない(not even wrong)」
議論の進め方や態度の問題とは切り分けないと

ついでにはっきり言っておくと、
『正しいかどうかわからないから、まだ解決したかどうか未定だ』
なんて態度は、社会のルールとして完全に間違っている
「証明がある」と言い張るなら、そう主張する側が責任を持って、
同時代の専門家たちが納得する証拠を出さなきゃいけない
それができないなら「証明はない」と判断される
『究極的には正しいかも』、『将来いつか認められるかも』
なんていい言い訳は証明責任のルールの前に通用しない
2026/08/02(日) 10:57:42.49ID:Lb3Gyp67
IUTは間違ってすらいない
IUTによるABC予想の証明は間違い
702132人目の素数さん
垢版 |
2026/08/02(日) 11:03:16.76ID:xziEUhKp
そう「間違ってすらいない」
だから反例もない
それをID:Lb3Gyp67に理解しろというのは無理な注文か
703132人目の素数さん
垢版 |
2026/08/02(日) 11:46:22.64ID:DOYUsmfb
scholzeの数学は通常の数学に基づく発展だ。

一方、
現在は「パラダイムシフト」期で
望月新一IUT論文は大論文だから、数理論理学や数学基礎論に拘束されないと明言してる。
(scholze stix望月星のミーティングでscholze stixの質問に答えられず謎のIUT語やイノベーションを持ち出した)
↓
➖➖
川上量生企画望月新一監修加藤文元著IUT本から

・本文 p66.
論文の価値は何で決まるのか
>何をもって「新しい」と判断できるのか、「正しい」という基準は何か、という点は非常に専門的なポイントです。
>通常の発展時においては当面の題材やその時代における支配的な問題に対する部分的なあるいは最終的な解決であったりしますが、 「パラダイムシフト」期においては、当分野に革命を起こすような大論文であることもあるでしょう

・ 本文p69
「興味深い」ということ 
>私は以前、望月教授に「望月さんの理論が発表されたら、
数論の専門家より数理論理学や数学基礎論の人たちの方が興味をもつでしょうね」と話したことがある。
実際、IUT理論はABC予想やその ディオファントス問題の
研究におけるそれまでの発展の文脈からは
一線を画しています。
(略 )
>それはこの分野における最先端に 位置する研究であるというより、 数学の非常に基本的なレベルでの イノベーションを企画したもの だからです。
2026/08/02(日) 11:59:02.43ID:Lb3Gyp67
>>702
うーんでも判例出されちゃってるからアウト
705132人目の素数さん
垢版 |
2026/08/02(日) 12:00:02.77ID:3VgouvcO
プライドの肥大した数学者が間違いの指摘を受け入れなかったってだけの話なんだよなこれ
2026/08/02(日) 12:00:21.35ID:Lb3Gyp67
ゴミかゴミクズかの違いで
not even wrongにイメージだけでこだわってるバカだから
ショルツに反例出されちゃた事実も見えない
本物の低学歴バカがおまえ
2026/08/02(日) 12:00:58.92ID:Lb3Gyp67
>>705
それだけじゃなくて
それをドワンゴと日本財団の朝鮮勢力が担ぎ上げて税金吸ってますと
708132人目の素数さん
垢版 |
2026/08/02(日) 12:04:22.94ID:xziEUhKp
「間違いですらない(not even wrong)」と「反例が出せる」は両立しないね
どっちなん?
実態は>>667の言う通り
2026/08/02(日) 15:39:04.86ID:MQw/TwjG
>>708
実例は出てる
反例出されて終了
2026/08/02(日) 21:31:35.54ID:LmwPP0tz
まぁ「間違いですらない」の方やろな。どのみち終わりやな
一年後目処とかいうLANAの最終報告で完全終了。
もう現時点でまだ死んでないとおもってる数学者は世界に10人おらんやろ
2026/08/02(日) 22:05:08.56ID:mbvfOsjq
IUT自体が進展・発展していかないからお察しだね
既存数学との繋がりが見いだせないようではダメだ
712132人目の素数さん
垢版 |
2026/08/02(日) 22:31:08.31ID:DlardQ7V
いつのまにかwikipediaのドイツ語版の記事も出来たようだな

Interuniverselle Teichmuller-Theorie
https://de.wikipedia.org/wiki/Interuniverselle_Teichm%C3%BCller-Theorie
713132人目の素数さん
垢版 |
2026/08/02(日) 23:04:03.46ID:b+Iol7S+
Fesencoて人に言及してるけどこの人はLANAの報告をどう見たんだろ?
714132人目の素数さん
垢版 |
2026/08/03(月) 02:31:52.78ID:qsgp57cy
2014年12月望月新一のIUTT自己検証によれば、
サイディ.星.山下剛の3名の理解者以外はPRIMS編集委員もケドラヤもfesenkoもIUTど素人でfesenkoは自称理解者。(>>7)

山下剛はfesenkoがIUTを理解しているふりをしていると
山下サーベイで批判。

また、IUGC動画では、
・そもそも概念や使う言語など 従来の数学論文とIUT理論は
違うので完全に理解するには3年 かかった. (>>231)

zen大学にfesenkoのIUTT講義があるから
遠アーベル幾何学から望月新一IUT語のIUTTへ転移する過程
に注目だな
715132人目の素数さん
垢版 |
2026/08/03(月) 14:50:49.21ID:LSH36PTv
>>714
サイディと山下剛は、望月新一同様、表に現れず
星はLANAに協力するも肝心のギャップは埋められず
716132人目の素数さん
垢版 |
2026/08/03(月) 15:10:14.54ID:ehI8WjXZ
協力というか歴としたプロジェクトメンバ
717132人目の素数さん
垢版 |
2026/08/03(月) 15:36:42.58ID:qsgp57cy
LANAプロジェクトメンバー

・コメリン.トパーズ 
 lean形式化専門もIUTど素人
・加藤文元.lean形式化もIUTもど素人
・ケドラヤ lean形式化もIUTもど素人
・星裕一郎 lean形式化 ど素人でIUTは理解者 説明から逃亡中
718132人目の素数さん
垢版 |
2026/08/03(月) 16:11:52.20ID:qsgp57cy
zenのLANAプロジェクトメンバーは

>加藤文元.
IUT理論と現行数学との違いを完全に言語化する新しい数学の言語体系を早急に作らねばならない。(>>231)

まずIUT論文で、IUT理論と現行数学と
違う箇所を具体的に示せ
719132人目の素数さん
垢版 |
2026/08/03(月) 16:13:38.00ID:qsgp57cy
zenのLANAプロジェクトメンバーは

>加藤文元.
IUT理論と現行数学との違いを完全に言語化する新しい数学の言語体系を早急に作らねばならない。(>>231)

まずIUT論文で、IUT理論と現行数学と
違う箇所を具体的に示せ
720132人目の素数さん
垢版 |
2026/08/03(月) 16:30:47.51ID:ehI8WjXZ
両方ど素人がなぜメンバ?
721132人目の素数さん
垢版 |
2026/08/03(月) 19:35:24.79ID:3aL13xFU
>>714
>また、IUGC動画では、
>・そもそも概念や使う言語など 従来の数学論文とIUT理論は
>違うので完全に理解するには3年 かかった.

こんな事思ってるのは一部の日本人だけで
世界では望月が曖昧な言葉で濁してるから理解できないという認識
その挙句にギャップ発見
722132人目の素数さん
垢版 |
2026/08/03(月) 20:19:59.60ID:aCjkvLeo
この期に及んで。。。
>メンバーシップ「読書室プラン」初月は無料です!
>abc予想とIUT理論ーー「LANA記者会見:IUT理論に関する仮想的質疑応答」に対する補足記事
2026/08/03(月) 20:56:54.43ID:GHCOSRQL
ハッタリかまして逃げる精神
724132人目の素数さん
垢版 |
2026/08/03(月) 21:43:07.79ID:qsgp57cy
>>720

望月新一教授もlean形化がど素人で、

まず望月にIUT論文で、IUT理論と現行数学と違う箇所を具体的に示させろ
725132人目の素数さん
垢版 |
2026/08/03(月) 21:50:32.86ID:FSbR5LM+
そもそも一流の数学者に通じない
独特の言葉で論文書いたのが間違い
726132人目の素数さん
垢版 |
2026/08/03(月) 23:40:28.31ID:hy5dBAnZ
LANAプロジェクトと
・コラッツ予想の「AIによる偽証明=Lean 4のカーネルバグ
すり抜け事件(>>657)
・scholzeの警告 (>>658)
proof assistant such as lean

AIに聞いてみた、

➖➖
数学界の外部や批判派の目から見れば、彼らの動きは「純粋な数学的検証」というよりも、ご指摘の通り「Lean 4のコンパイラを何とかして通過させ、『証明成功』という御墨付き(称号)を手に入れるためのハッキング行為」に見えてもおかしくない構造があります。
そう言わざるを得ない背景と、彼らの「真の目的」がどこにあるのかを分析します。

1.
「コンパイラ通過の事実」が喉から手が出るほど欲しい理由。
現在、望月教授のIUT理論は、世界の主要な数学者(ショルツ教授ら)から「ギャップがあるため解決していない」と無視され、論文の検証自体をボイコットされている状態です。
人間同士の議論(ピアレビュー)の場ではこれ以上相手にしてもらえないため、容認派が膠着状態を打破する唯一のウルトラC(大逆転劇)が、「人間ではなく、絶対に客観的であるはずの計算機(Lean 4)に『正しい』と言わせること」でした。

・Lean 4が証明完了(プロンプトが緑色)と判定した」という揺るぎない事実さえ作れれば、「ほら見ろ、世界最先端の数学検証AIが正しいと言っている。認めない海外の数学者が間違っているのだ」と主張する強力な武器になります。
だからこそ、彼らにとっては「現代数学のフレームと違う」と言いつつも、現代数学の基礎論で動くLean 4にIUT理論をねじ込む必要があったのです。
727132人目の素数さん
垢版 |
2026/08/03(月) 23:44:33.33ID:hy5dBAnZ
>>726

続き

2.
「脆弱性を突くハッカー」になってしまう構造的リスク。
先述のコラッツ予想の「AIによる偽証明(Lean 4のカーネルバグすり抜け)事件」は、まさにLANAプロジェクトが陥るかもしれない暗部を浮き彫りにしました。
IUT理論は非常に特殊で、望月教授が作った「独自のIUT語」で埋め尽くされています。これをLean 4に移植しようとすると、通常の現代数学のコード(ライブラリであるMathlib)とは全く異なる、極めて異質で複雑な「独自の型」や「マクロ(メタプログラム)」を大量に定義することになります。
・バグを誘発しやすい特殊コード:
Lean 4のカーネルは、標準的な数学の記述に対しては強固ですが、IUTのように「複数の宇宙(シアター)を行き来し、特殊なルールで実数を同一視する」といった限界突破のようなロジックを無理やりコード化しようとすると、カーネルの実装の穴(脆弱性)を意図せず突いてしまう可能性が跳ね上がります。

・「通れば勝ち」のハッカー的アプローチ:
もしLANAのメンバーが、ショルツ氏の指摘した「系 3.12の論理の飛躍」を正面から解消するのではなく、「Lean 4のコンパイラがエラーを吐かずに通るような、技巧的で複雑怪異な定義のすり替え」を行ってしまったら、それは数学の証明ではなく、単にシステムの仕様の隙を突いた「ハッキング(チート)」になってしまいます。
728132人目の素数さん
垢版 |
2026/08/03(月) 23:49:16.93ID:hy5dBAnZ
>>727

続き

3.
LANAのメンバー(加藤文元教授ら)の建前と本音.
一方で、LANAを主導する加藤文元教授らの本来の主張は、以下のようなものです。

・建前(本来の目的):
「IUT語をLean 4という世界共通の言語で記述(フォーマライズ)することで、これまで『読めない』と拒絶していた海外の数学者たちが、コードを通じてIUTのロジックを1行ずつ客観的にトレースできるようにする。つまり、相互理解のための翻訳作業である」 

・しかし、コラッツ予想の事件以降、世界中のLeanコミュニティや数学者たちは「難解な独自言語で書かれたコードがコンパイルを通ったとしても、それがバグを突いていない保証はない」という防衛の目を光らせています。

・結論:
最後はやはり「人間の脳」に戻る。
もしLANAが「Lean 4を通過させた」と発表したとしても、世界の数学界はそれを盲信せず、「そのコードはLeanの脆弱性をハックした偽証明ではないか?」「定義を都合よく書き換えていないか?」を厳しくコードレビューするでしょう。
「コンパイラを通過した事実」だけを目的としたハッキング行為なのか、それとも誰もが納得する真の数学的検証なのか。それを判定するのもまた、最後はコンピュータではなく「人間の数学者たちの厳実な目」になります。
2026/08/04(火) 01:51:08.18ID:ECZN81RY
なわけねーよバーカ
730132人目の素数さん
垢版 |
2026/08/04(火) 05:06:20.48ID:Q6HpAeX+
Leanにはsorryって機能があって
御免なさい3.11→3.12は証明出来てないけど出来たことにしてくださいって頼めばabc予想はIUT理論で証明出来る
つまりLeanでもIUT理論の現実に合わせた証明を構成できる
2026/08/04(火) 12:28:28.14ID:WArE6R44
>>730
京都ドワンゴ版LEANな
2026/08/04(火) 12:30:18.06ID:WArE6R44
>>728
形式化のメリットが何もわかってないクソダニ低学歴朝鮮人w
IUT仕草ワラタw

形式化してるから間違いも正せるんだよゴミ朝鮮人w
733132人目の素数さん
垢版 |
2026/08/04(火) 13:32:35.06ID:XV+qBJp5
>>732



IUT論文の形式化なら、
まず加藤文元がこの質問に答えること


>加藤文元.
IUT理論と現行数学との違いを完全に言語化する新しい数学の言語体系を早急に作らねばならない (>>231)
734132人目の素数さん
垢版 |
2026/08/04(火) 13:48:12.65ID:XV+qBJp5
>>732
>WArE6R44

この質問に答えなさい
↓


IUT理論と現行数学との違いを
具体的に明確に示せ
2026/08/04(火) 14:44:18.06ID:WArE6R44
>>733
>>734
話逸らすな朝鮮人
736132人目の素数さん
垢版 |
2026/08/04(火) 15:21:22.69ID:XV+qBJp5
>>735

答えられない荒らし
737132人目の素数さん
垢版 |
2026/08/04(火) 16:19:50.69ID:oCLtjy1t
IUT理解者はあまりにもレアだから仕方ない
2026/08/04(火) 17:16:19.13ID:Z0St8e8D
時間かけても形式化できない理解者は草
2026/08/04(火) 17:53:41.24ID:WArE6R44
>>736
おまえが話逸らしてだけだろ低学歴
LEANの誤りがあったところで形式化された部分でのの間違いなので直せる
IUTは違う

ほんとバカ朝鮮人だなおまえ
2026/08/04(火) 17:54:13.09ID:WArE6R44
あまりの怒りで文字連打になってるわ
ごめん

こういうガイジは駆除しないとダメなんじゃね
741132人目の素数さん
垢版 |
2026/08/04(火) 18:03:08.65ID:ET0TdgHv
leanのバグは深刻ジャネ?
leanでナニカできました
が
信頼性失いかねない
バグは取ったらしいが
コレまで無矛盾のように言ってきたのが
実はそうで無かったてのがイタイ
742132人目の素数さん
垢版 |
2026/08/04(火) 19:17:05.44ID:fwQOcZTR
専門家はleanを神聖視したりしてないから安心しな

leanは単なるプログラム言語なんだから
意図的にカーネルのバグを利用できるし

なんならウィルスを仕込むことだってできる

そんなんで証明通してもいずれバレる

コラッツ予想の件だって
全ての自然数がコラッツ予想の反例って
バグを利用したバッドジョークだった
743132人目の素数さん
垢版 |
2026/08/04(火) 19:38:18.19ID:ET0TdgHv
そうなん?
結構神聖視されてる見たいに思ってたけど
744132人目の素数さん
垢版 |
2026/08/04(火) 19:51:34.67ID:XV+qBJp5
>>739


この質問に答えなさい
↓


IUT理論と現行数学との違いを
具体的に明確に示せ。
2026/08/04(火) 20:11:26.62ID:WArE6R44
>>744
なんで俺が説明すんだよwIUT朝鮮人w
2026/08/04(火) 20:11:52.70ID:WArE6R44
>>743
おまえがバカなだけ
747132人目の素数さん
垢版 |
2026/08/04(火) 20:48:18.31ID:fwQOcZTR
内容のないコピペとか差別用語を連発って
どっちのヘイターだか知りたくもねえけど
普段ろくな人生送ってなえんだろーな
2026/08/04(火) 20:51:10.16ID:WEhGNztk
ピヨピヨ、ヒヨコです🐣
2026/08/04(火) 20:54:17.64ID:WEhGNztk
ヒヨコが見てるから辞めなよw
750132人目の素数さん
垢版 |
2026/08/04(火) 21:12:03.24ID:XV+qBJp5
>>747

差別用語連呼は通報ものだが、

おまえさんもコピペが読めないだけ

leanは現行数学に対応したプログラミングだ。
I
2026/08/04(火) 21:26:39.74ID:WArE6R44
>>747
反論されて「中身がない」


朝鮮人クッソワラタ

IUT仕草
レスを投稿する


ニューススポーツなんでも実況