Inter-universal geometry とABC 予想55

Inter-universal geometry とABC 予想55 at MATH

348:１３２人目の素数さん
24/04/30 18:33:18.01 MP9Ztl9L.net
屏風の中の虎、が宇宙際の実態だね
どれだけエラい人が、何百ページ書こうと、トンデモはトンデモです

349:１３２人目の素数さん
24/04/30 18:37:29.65 i/HxGRCZ.net
>>348
用語の本当の理解

350:１３２人目の素数さん
24/04/30 19:29:06.34 vUXRw3n0.net
皆知ってたか？
文元のIUT本が角川ソフィア文庫になってるの。ビビったわ

351:１３２人目の素数さん
24/04/30 20:44:13.41 2xE2nHAU.net
>>346-347
>Scholzeさんの例は有名すぎるのでもう一つ。。。Tim GowersさんやTerence TaoさんのMarton conjecture>解決の論文も、Lean4での形式化が企画されてますね。
>[URLﾘﾝｸ(terrytao.wordpress.com)

・いいね。それありかも
・つまり、川上懸賞金の100万ドル（1.5億円）を狙って
　コンピュータ検証にかける
・IUTがダメなら懸賞金ゲット！
　IUTが白でも、それなりに賞貰えそう（10万ドル（1.5千万円））
・やった人は、一躍有名人だ

352:１３２人目の素数さん
24/04/30 20:52:19.69 O16KksZM.net
>>351
iutはそれすらできないほどに酷い

353:１３２人目の素数さん
24/04/30 20:54:22.09 2xE2nHAU.net
Lean (proof assistant)か
URLﾘﾝｸ(en.wikipedia.org)(proof_assistant)
Lean (proof assistant)
Usage
Mathematics
See also: Proof assistant § Notable formalized proofs
Lean has received attention from mathematicians such as Thomas Hales[11] and Kevin Buzzard.[12] Hales is using it for his project, Formal Abstracts.[13] Buzzard uses it for the Xena project.[14] One of the Xena Project's goals is to rewrite every theorem and proof in the undergraduate math curriculum of Imperial College London in Lean.
In 2021, a team of researchers used Lean to verify the correctness of a proof by Peter Scholze in the area of condensed mathematics. The project garnered substantial attention for formalizing a result at the cutting edge of mathematical research.[15] In 2023, Terence Tao used Lean to formalize a proof of the Polynomial Freiman-Ruzsa (PFR) conjecture, a result published by Tao and collaborators in the same year.[16]
Artificial intelligence
In 2022, OpenAI created a neural network-based theorem prover for Lean, which used a language model to generate proofs of various high-school-level olympiad problems.[17]
Later that year, Meta AI created an AI model that has solved 10 International Mathematical Olympiad problems; this model is available for public use with the Lean environment.[18]
URLﾘﾝｸ(ja.wikipedia.org)(%E8%A8%BC%E6%98%8E%E3%82%A2%E3%82%B7%E3%82%B9%E3%82%BF%E3%83%B3%E3%83%88)
Lean (証明アシスタント)
歴史
Lean はGitHubでホストされているオープンソース（英語版）プロジェクトである。2013年にMicrosoft ResearchのLeonardo de Mouraによって立ち上げられた[1]。Lean 2 では Homotopy Type Theory (HoTT) をサポートしていた。[2] しかし後の Lean 3 以降ではHoTT のサポートは Lean 言語の標準ライブラリから削除された。[3]
利用
Kevin Buzzard は、数学者や数学科の学部生の間で Lean のような定理証明支援系を普及させることを目指す Xena プロジェクトを主導している。[10]Xena プロジェクトの目標の1つは、インペリアル・カレッジ・ロンドンの学部生の数学カリキュラムにあるすべての定理と証明をLeanで書き直すことである。
2020年12月、数学者の Peter Scholze は自身の liquid vector space に関する定理を Lean で形式化することは可能かという挑戦状を Lean コミュニティに持ち込んだ。この挑戦は Liquid Tensor Experiment と呼ばれ、2022年7月に完了が宣言された。[11]
フィールズ賞受賞者の Terence Tao は、2023年10月のSNSへの投稿で、自身の論文を Lean 4 で形式化する過程で小さな（しかし非自明な）ミスを見つけることができたと明かしている。[12]

354:１３２人目の素数さん
24/04/30 21:05:54.49 2xE2nHAU.net
>>352
あほなことを連発すると、信用されないよ
・普通は、まずIUTの分量が多すぎるってことでしょ？問題は
・二つ目に、従来の数学用語を独自にひねってあるので、既存のライブラリーが生きない
・三つ目に、準備論文もインプットしないとだめだろうってこと
なので、コンピュータにかける前処理が膨大になるので簡単ではなかったのです
しかし、近年の生成AIのサポートがうまく使えるかもしれない
それは、狙い目と思うよ

355:１３２人目の素数さん
24/04/30 21:09:40.69 jLqb28pG.net
アホはお前だ
理解不能なものを形式化できるわきゃない

356:１３２人目の素数さん
24/04/30 21:32:40.45 LjGOyP17.net
>>334
デマはやめましょう。
PRIMS編集委員会は全く
新しい理論IUTTのIUT論文として
受理した。
された。

357:１３２人目の素数さん
24/04/30 21:41:36.00 2xE2nHAU.net
>>355
・高等数学は、理解できる人も理解できない人もいて当然
　だれかが、理解できないと言っても、当然
・数学の投稿論文の理論に、新規性があるのは当然
　いまさら何をいうかｗ

358:１３２人目の素数さん
24/04/30 21:42:57.19 2xE2nHAU.net
リンク訂正
 >>355
　↓
>>355-356

359:１３２人目の素数さん
24/04/30 21:43:14.88 doVY1jXx.net
>>354
じゃあんたがやったら？

360:１３２人目の素数さん
24/04/30 21:44:17.84 LjGOyP17.net
>>356
2020年4月3日
PRIMS特別編集委員会委員長.
IUT論文受理の記者会見
玉川安騎男教授
「IUTTは全く新しい理論　」毎日　
「査読の過程はお墓に持っていく」

361:１３２人目の素数さん
24/04/30 21:44:42.77 O16KksZM.net
そう、iut論文の本質的問題は“意味不明”である事
基礎論の研究で標準化された数学による証明はrecursive、つまりそれが正しい証明かどうか計算機で判定できるように作られている、計算機すらない時代に、天才達の知恵の結晶
しかしそれもこれも、その文章が標準の数学の言語ルールに従う文章を自然言語に標準的な方法で変換されたものの場合に限る
そもそもiutという数学の言語も推論規則も公理も何も規定されていない、しかもそれを自然言語で表されてるからどうしようもない

362:１３２人目の素数さん
24/04/30 21:56:26.87 MP9Ztl9L.net
ただのカルト、虚偽数学

363:１３２人目の素数さん
24/04/30 22:16:39.66 LjGOyP17.net
NHKスペシャル
数学者は宇宙をつなげるか？ａｂｃ予想証明をめぐる数奇な物語
2022年4月10日
・玉川 RIMS教授.PRIMS特別編集委員会委員長　
「いわば現代の数学では、禁じ手になってるようなことも取り入れて、
何かできないかということを考えたということなんですね。
1＋1は2でありながら、1＋1は5であるとか。
二つの直線が交わるということが起こりながら交わらないとか。
本来だったら矛盾が起こるようなことを、活用できないかと考えた」

364:１３２人目の素数さん
24/04/30 22:26:51.25 aEpVe/D7.net
結局Leanって万能に近いツールなのか？
人間の数学者いらなくなるじゃん

365:１３２人目の素数さん
24/04/30 22:35:23.85 2xE2nHAU.net
１）Leanとか万能に近いツールが出来ても、それを使いこなすのは人間
２）数学者は、Leanを使って数学を研究したり、たまに間違うLeanを正す仕事があるだろう

366:１３２人目の素数さん
24/04/30 22:37:20.84 2xE2nHAU.net
本来だったら矛盾が起こるようなことを、活用できないかと考えたが
結局、従来の種の理論と圏論の範囲でおさまったんじゃないの

367:１３２人目の素数さん
24/04/30 22:41:15.39 MP9Ztl9L.net
本来だったら矛盾が起こるようなことを、活用できないかと考えた。
ーーー結果、トンデモ化してしまった。
まあ望月からは謙虚に人の話を聞いたり勉強したりする態度は微塵も感じられないないからね。
そういう人が土地勘のないところに手を出すとトンデモ化してしまうもの
数学通信の怪文書とかもひどかっただろ？笑

368:１３２人目の素数さん
24/04/30 22:42:14.57 LjGOyP17.net
>>366
あらしのトンデモくん
巣へ帰れ