26/05/26 17:21:20.39 AA1mxJDj.net
要するに、形式化に手こずってるって事？
162:名無しのひみつ
26/05/26 18:11:29.40 FWkx+wJI.net
いや証明が間違ってたからグズグズしてるだけ
形式化なんてあそこまでヒューマンリソース注ぎ込んだらもう終わってるって
163:名無しのひみつ
26/05/26 18:27:23.38 saGjBzkj.net
LEANは過去の数学に基づいて作られた検証ツール
LEANの枠組みを超えるような新数学理論だってあり得るだろう
それが画期的で新しい物であればあるほど
164:名無しのひみつ
26/05/26 18:49:07.19 HDdDuoyG.net
IUTはそういうものではないんだよ
望月も頭の切り替えが必要なだけで簡単だと言ってるだろ
165:名無しのひみつ
26/05/26 21:36:00.25 GBfEmR7b.net
>>163
ゲラゲラ
ほんとバカチョンの言い訳は終わってるわ
166:名無しのひみつ
26/05/28 16:07:53.44 NB/plnTP.net
どっかで見た手口
33 名無しさん＠実況は禁止ですよ 警備員[Lv.3] (ﾜｯﾁｮｲ 1347-h4v0) 2026/05/27(水) 15:02:09.76 ID:KVhGBc830
今日Xのタイムラインでやたらとニコニコ動画を褒めまくってる（よいしょ）ポストが流れてるんだけど、ニコニコを褒め称えるバイトでもあるのかな
今までの運営を全然しらない人がポストしてるようなのばっかり
URLﾘﾝｸ(egg.5ch.io)
40 名無しさん＠実況は禁止ですよ 警備員[Lv.0][新芽] (ﾜｯﾁｮｲ ab0c-S3fo) 2026/05/28(木) 14:05:00.35 ID:w+lIvLur0
>>33
まじなんなんだろうなあれ、最近流れてきてきっしょいわ
だれか言ってやれよ、糞運営は相変わらずだと
URLﾘﾝｸ(egg.5ch.io)
167:名無しのひみつ
26/05/29 05:20:30.24 /JTGW/12.net
>>163
数学基礎論を余り分かってないのでは
数学の理論は
1.推論規則
2.公理的集合論
3.対象とする分野の公理
から成り立っている
IUTは二階述語論理+ZFCAに収まることは一連の報道で明らかで
1と2に関して新しいことは必要としてない
だからLeanで記述出来ることは明らか
なお2に関してはいろいろ選択肢がないわけではない
1に関しても選択肢はある
一般的に言ってどんな新しい数論の理論でも
ZFCAの範囲に収まってしまう
それくらい人間が関心のある公理系は非常に狭い
公理系を記述する言語が生成する公理系群全体に比べると
168:名無しのひみつ
26/05/29 10:22:35.91 bTLOf4IY.net
朝鮮人「一連の報道から明らか」
朝鮮人「Leanで記述できることは明らか」
キチガイ朝鮮人妄想w
報道ww
169:名無しのひみつ
26/05/29 16:31:54.76 7o4BeZv5.net
xyz予想の方もどうかよろしく
170:名無しのひみつ
26/05/29 19:47:42.80 3oL+i+5G.net
阿部氏巨人監督止そう問題
171:名無しのひみつ
26/05/31 12:12:53.47 aiiQNSId.net
select
count(*),
a, b, c,
rad(abc) as d
from universe
where
a + b = c
and
c > d^(1+ε)
and
ε > 0;
172:名無しのひみつ
26/05/31 14:17:17.12 EiyTUZab.net
同じ系統のドワンゴ国産LLMのオッサンもいい感じに仕上がってきたなw
訴訟がどうの喚き始めたw
173:名無しのひみつ
26/06/02 13:09:25.41 X6YsZBx5.net
5chには理解者が多数いるのになんで世界の名だたる数学者は理解できないんだ…
174:名無しのひみつ
26/06/12 00:24:42.99 VUQlXnQM.net
URLﾘﾝｸ(sites.google.com)
ZMCやRIMSの人も出るのね
しかし何も聞こえてこないなあ
175:名無しのひみつ
26/06/16 13:49:35.54 E78Ln7oY.net
角川歴彦（ＫＡＤＯＫＡＷＡ元会長）、夏野剛を提訴wwwwwwwwwwwwwwwwwwwwwwwww [398059782]
URLﾘﾝｸ(greta.5ch.io)
176:名無しのひみつ
26/06/19 10:41:22.02 8CBPqJo3.net
>>174
来来週始め開始だから10日切ったね
>>33
>7月17日に中間報告会を開き、研究成果などを公表する考えだ。
これも1月切った
2年やってまだ中間報告か
177:名無しのひみつ
26/06/19 17:01:46.98 ATytdxHc.net
数学の人間が書いた普通の論文を、AIの力によってLeanで記述させれば、証明の検証が機械的にできたりはせんのか？
178:名無しのひみつ
26/06/19 18:16:34.63 xxBbVc27.net
>>177
形式化が難しい
ギャップがあるから
つまり理論が間違ってるから出来ないだろうね
数学に親しんでないと
形式化が済んで形式推論で真偽をはっきりさせると
正しいか間違ってるか分かるだろと思うだろう
けどその必ず真偽が分かるというのは完全性と言って
ゲーデルが数論を含めば数学理論は完全性を持たないと証明している
つまりそうはならない
要するに>>81
179:名無しのひみつ
26/06/28 18:58:32.99 1AGGs48A.net
Fumiharu Kato 加藤文元（Bungen）
@FumiharuKato 20時間
Hodge-Arakelov理論の大域化によってabc予想が解けるかもしれないという病気にかかった人が、数学史上2人だけいた。1人はMochizukiで、もう1人がKimだ。
Fumiharu Kato 加藤文元（Bungen）
@FumiharuKato 20時間
昨日までエディンバラにいた。欧州は記録的熱波ということでエディンバラもスコットランドらしからぬ焼け付くような晴天だったが風は冷たく過ごしやすかった。Minhyong Kimの家でいろいろお話しした。私は何と戦っているのか、途中でわからなくなっていたが、最後にはまたわかって帰国した。
180:名無しのひみつ
26/06/29 10:15:22.57 1OpGRuUB.net
>>179
RIMS外のIUT擁護者たちに証明にギャップがあるという結論について意見交換して
最終的に同意しなかったのが望月と金だということなんだろうな
違うの？
181:名無しのひみつ
26/06/29 17:51:25.94 nDGbHzkE.net
メイドさん ご苦労さん