大学の数学が期待したほど面白くなかったんだが

**１３２人目の素数さん** · 2023/11/25(土) 20:49:57.46

**１３２人目の素数さん** · 2023/11/30(木) 21:55:35.98

字が小さくてスマホで読むのつらいンゴ

**１３２人目の素数さん** · 2023/11/30(木) 22:02:12.98

軽く読んだけど、これが上でやってた話とどう関係してるのかわからん
Coqで四色定理とかodd order theoremとかと何か違うようには見えないんだが

**１３２人目の素数さん** · 2023/11/30(木) 22:08:21.70

>>82
情報thx

**１３２人目の素数さん** · 2023/11/30(木) 22:28:10.65

ソース眺めてみればわかるけど、これは結局のところ130年前にラッセルが手作業でやってたことと同じやろ。違いは計算機が検証してくれるかだけや
https://github.com/leanprover-community/lean-liquid/blob/master/src/condensed/short_exact.lean

**１３２人目の素数さん** · 2023/11/30(木) 23:26:54.57

>>82
それもまるでダメだってw

**１３２人目の素数さん** · 2023/11/30(木) 23:28:07.53

>>80
具体的には基礎数学読んでからにしてねってこと

**１３２人目の素数さん** · 2023/11/30(木) 23:38:24.61

Condenced mathの話は証明が恐らくできていると思われたが非常に複雑なので計算機でチェックしてもらったという内容だったかと

**１３２人目の素数さん** · 2023/11/30(木) 23:41:54.39

無限にある数学的に真な命題のうち数学的に意味のあるものはほんの一部だからね
AIにその判断をさせるのは厳しいよ
というのも人間だってその数学的意味とはなんなのかハッキリ定義できないんだから

**１３２人目の素数さん** · 2023/11/30(木) 23:54:42.27

chatgpt3.5の場合だが、解が1つもない方程式
(解がないことは高校数学で簡単に示せる)を出題してみると、
chatgpt3.5は「これが解です」とデタラメな解を捏造してくる。

人間側が「間違ってるよ」とだけ指摘すると、chatgpt3.5は
「すみません。これが本当の解です」と別のデタラメな解を捏造してくる。

この作業、何度繰り返しても同じで、
解が1つもないことにchatgpt3.5が気づくことはなく、
延々とデタラメな解を捏造してくる。

**１３２人目の素数さん** · 2023/11/30(木) 23:56:28.33

従って、chatpgt3.5の回答が正しいかどうかをchatpgt3.5自身が
検証するようにプログラムした場合、chatpgt3.5は

「これが解だ」→「いや違ったわ」→「これが解だ」→「いや違ったわ」→・・・

という無限ループに陥るはず。
適当な回数で打ち切れば無限ループは回避できるが、そのかわり、
最終的に出力された回答は依然としてデタラメな回答ということになる。

こういう問題、AI側はどうやって対処したらいいのか？
言うまでもなく、完璧な対処法は存在しない。
なぜなら、それができたら停止性問題が決定不能であることに矛盾するからだ。

**１３２人目の素数さん** · 2023/12/01(金) 00:00:46.56

直観的に言えば、与えられた数学の問題の「複雑性」が
決定不能問題の複雑性に肉薄すればするほど、
AIは無限ループに陥りがちになるはず。
しかも、数学ではそのような事象が起こりやすい。
問題文の一部を変えただけで難易度が激変するからだ。

尤も、AIが数学の問題を解けなくなっていくことは
人間にとっても同様であり、難しい数学の問題ほど、人間だって歯が立たない。

そんな状況下で、AIは人間よりもマシな回答(しかし結局はデタラメな回答)を
出力できるようになるのだろうか？

**１３２人目の素数さん** · 2023/12/01(金) 00:07:43.73

ここで言う

＞人間よりもマシな回答(しかし結局はデタラメな回答)

とは、

「数学的には間違った解答だが、そのアイデアには新規性があり、
　新しい数学が創出できそうだ」

という意味。このレベルに妥協するなら、そのうち可能になるかもしれない。
ただし、それは数学者が仕事を失うことを意味しない。

**１３２人目の素数さん** · 2023/12/01(金) 00:14:24.61

もしかしたらラマヌジャンみたいなのが生まれるかもね

**１３２人目の素数さん** · 2023/12/01(金) 00:39:11.21

これが自動証明できる？

∃N,s,p,m,P,g(φ∈N
　∧s∈N×N
　∧∀a∈N∃b∈N([a,b]∈s)
　∧∀a,b,c∈N([a,b],[a,c]∈s→b=c)
　∧∀a∈N(￢[a,φ]∈s)
　∧∀M⊂N(φ∈M
　　∧∀a∈M∃b∈M([a,b]∈s)
　　→M=N)
　∧p∈N×N×N
　∧∀a,b∈N∃c∈N([a,b,c]∈p）
　∧∀a,b,c,d∈N([a,b,c],[a,b,d]∈p→c=d)
　∧∀a∈N([a,φ,a]∈p)
　∧∀a,b,c∈N∃d,e∈N([b,d],[c,e]∈s
　　∧ （[a,b,c]∈p→[a,d,e]∈p))
　∧m∈N×N×N
　∧∀a,b∈N∃c∈N([a,b,c]∈m）
　∧∀a,b,c,d∈N([a,b,c],[a,b,d]∈m→c=d)
　∧∀a∈N([a,φ,φ]∈m)
　∧∀a,b,c∈N∃d,e∈N([b,d]∈s
　　∧[a,c,e]∈p
　　∧([a,b,c]∈m→[a,d,e]∈m))
　∧P⊂N
　∧∀q∈P∀b,c∈N([b,c,q]∈m→[φ,b]∈s∨[φ,c]∈s)
　∧g∈N×N
　∧∀a∈N([a,a]∈g)
　∧∀a,b∈N∃c∈N([b,c]∈s
　　∧([a,b]∈g→[a,c]∈g∧￢[c,a]∈g))
　∧∀n∈N(n≠φ∧￢[φ,n]∈s→∃q∈P∃m∈N([n,n,m]∈p
　　　∧n≠q
　　　∧m≠q
　　　∧[n,q]∈g
　　　∧[q,m]∈g)))

**１３２人目の素数さん** · 2023/12/01(金) 00:42:03.88

全ての暗号は有限だから必ず解ける
リソース的に無理ってだけ
つまるところ ID:cs8MUWrU は
「1+1が計算できたぞ
これでどんな暗号も解ける」
って言ってるようなもんだと思うよ

**１３２人目の素数さん** · 2023/12/01(金) 00:43:36.25

ちょっと違うか
「どんな暗号も解けるんだぞ怖いか？」
かな

**１３２人目の素数さん** · 2023/12/01(金) 04:23:18.41

>>97
>これが自動証明できる？
随分間違えてた
これで
↓

N,s,p,m,P,g(φ∈N
　∧s⊂N×N
　∧∀a∈N∃b∈N([a,b]∈s)
　∧∀a,b,c∈N([a,b],[a,c]∈s→b=c)
　∧∀a∈N(￢[a,φ]∈s)
　∧∀M⊂N(φ∈M
　　∧∀a∈M∃b∈M([a,b]∈s)
　　→M=N)
　∧p⊂N×N×N
　∧∀a,b∈N∃c∈N([a,b,c]∈p）
　∧∀a,b,c,d∈N([a,b,c],[a,b,d]∈p→c=d)
　∧∀a∈N([a,φ,a]∈p)
　∧∀a,b,c∈N∃d,e∈N([b,d],[c,e]∈s
　　∧([a,b,c]∈p→[a,d,e]∈p))
　∧m⊂N×N×N
　∧∀a,b∈N∃c∈N([a,b,c]∈m）
　∧∀a,b,c,d∈N([a,b,c],[a,b,d]∈m→c=d)
　∧∀a∈N([a,φ,φ]∈m)
　∧∀a,b,c∈N∃d,e∈N([b,d]∈s
　　∧[a,c,e]∈p
　　∧([a,b,c]∈m→[a,d,e]∈m))
　∧P⊂N
　∧∀q∈P∀b,c∈N([b,c,q]∈m→[φ,b]∈s∨[φ,c]∈s)
　∧g⊂N×N
　∧∀a∈N([a,a]∈g)
　∧∀a,b∈N∃c∈N([a,c]∈s
　　∧([a,b]∈g→[c,b]∈g∧￢[b,c]∈g))
　∧∀n∈N(n≠φ∧￢[φ,n]∈s→∃q∈P∃m∈N([n,n,m]∈p
　　　∧￢[n,q]∈g
　　　∧￢[q,m]∈g)))

**１３２人目の素数さん** · 2023/12/01(金) 04:27:49.34

頭が消えてた
これで
↓

∃N,s,p,m,P,g(φ∈N
　∧s⊂N×N
　∧∀a∈N∃b∈N([a,b]∈s)
　∧∀a,b,c∈N([a,b],[a,c]∈s→b=c)
　∧∀a∈N(￢[a,φ]∈s)
　∧∀M⊂N(φ∈M
　　∧∀a∈M∃b∈M([a,b]∈s)
　　→M=N)
　∧p⊂N×N×N
　∧∀a,b∈N∃c∈N([a,b,c]∈p）
　∧∀a,b,c,d∈N([a,b,c],[a,b,d]∈p→c=d)
　∧∀a∈N([a,φ,a]∈p)
　∧∀a,b,c∈N∃d,e∈N([b,d],[c,e]∈s
　　∧([a,b,c]∈p→[a,d,e]∈p))
　∧m⊂N×N×N
　∧∀a,b∈N∃c∈N([a,b,c]∈m）
　∧∀a,b,c,d∈N([a,b,c],[a,b,d]∈m→c=d)
　∧∀a∈N([a,φ,φ]∈m)
　∧∀a,b,c∈N∃d,e∈N([b,d]∈s
　　∧[a,c,e]∈p
　　∧([a,b,c]∈m→[a,d,e]∈m))
　∧P⊂N
　∧∀q∈P∀b,c∈N([b,c,q]∈m→[φ,b]∈s∨[φ,c]∈s)
　∧g⊂N×N
　∧∀a∈N([a,a]∈g)
　∧∀a,b∈N∃c∈N([a,c]∈s
　　∧([a,b]∈g→[c,b]∈g∧￢[b,c]∈g))
　∧∀n∈N(n≠φ∧￢[φ,n]∈s→∃q∈P∃m∈N([n,n,m]∈p
　　　∧￢[n,q]∈g
　　　∧￢[q,m]∈g)))

**１３２人目の素数さん** · 2023/12/01(金) 04:30:43.97

ごめん重複があった
これで
↓

∃N,s,p,m,P,g(φ∈N
　∧s⊂N×N
　∧∀a∈N∃b∈N([a,b]∈s)
　∧∀a,b,c∈N([a,b],[a,c]∈s→b=c)
　∧∀a∈N(￢[a,φ]∈s)
　∧∀M⊂N(φ∈M
　　∧∀a∈M∃b∈M([a,b]∈s)
　　→M=N)
　∧p⊂N×N×N
　∧∀a,b∈N∃c∈N([a,b,c]∈p）
　∧∀a,b,c,d∈N([a,b,c],[a,b,d]∈p→c=d)
　∧∀a∈N([a,φ,a]∈p)
　∧∀a,b,c∈N∃d,e∈N([b,d],[c,e]∈s
　　∧([a,b,c]∈p→[a,d,e]∈p))
　∧m⊂N×N×N
　∧∀a,b∈N∃c∈N([a,b,c]∈m）
　∧∀a,b,c,d∈N([a,b,c],[a,b,d]∈m→c=d)
　∧∀a∈N([a,φ,φ]∈m)
　∧∀a,b,c∈N∃d,e∈N([b,d]∈s
　　∧[a,c,e]∈p
　　∧([a,b,c]∈m→[a,d,e]∈m))
　∧P⊂N
　∧∀q∈P∀b,c∈N([b,c,q]∈m→[φ,b]∈s∨[φ,c]∈s)
　∧g⊂N×N
　∧∀a∈N([a,a]∈g)
　∧∀a,b∈N∃c∈N([a,c]∈s
　　∧([a,b]∈g→[c,b]∈g∧￢[b,c]∈g))
　∧∀n∈N(n≠φ∧￢[φ,n]∈s→∃q∈P∃k∈N([n,n,k]∈p
　　　∧￢[n,q]∈g
　　　∧￢[q,k]∈g)))

**１３２人目の素数さん** · 2023/12/01(金) 05:00:38.70

アタオカ湧いてて草ｗｗｗ

**１３２人目の素数さん** · 2023/12/01(金) 07:14:16.89

>>103
あらあらw

**１３２人目の素数さん** · 2023/12/01(金) 07:44:14.07

あらあら

**１３２人目の素数さん** · 2023/12/01(金) 08:06:18.60

>>98
計算不可能性について勉強した方がいい

**１３２人目の素数さん** · 2023/12/01(金) 09:19:13.64

このスレは>>44で終わりました

**１３２人目の素数さん** · 2023/12/01(金) 12:04:00.46

>>106
そこは喩えね

**１３２人目の素数さん** · 2023/12/01(金) 13:02:15.39

>>94
それはちょっと面白い話だけど、多分AIはまず形式化されたデータ学習で生産的な
数学から攻略していくようにチューニングされるんじゃないかな
これは>>91と合わせて決定的な山だとは思う
数学的な意味や価値を自律的にかぎ分けるようになってくると一気に革命となるん
じゃないか

例えば関数体で出来たことは代数体で簡単に一般化できないという知識を出せるなら
、更にそれを入力にして探索を進めるような振る舞いはできるだろうし

**１３２人目の素数さん** · 2023/12/01(金) 13:20:37.91

代数幾何なんかやってると思うけど、これだけ定義に手間暇かかるのにこれくらいのことしか言えんのか。。
ってなる

**１３２人目の素数さん** · 2023/12/01(金) 13:33:58.24

>>97　>>100－102　φが束縛されてないが・・・

**１３２人目の素数さん** · 2023/12/01(金) 14:28:57.24

>>111
うむ確かに
∃φ∀a(￢a∈φ)
追加で
あとPに1入っちゃうけど関係ないからこのままで

**１３２人目の素数さん** · 2023/12/01(金) 14:36:10.80

そうか別に空集合で無くてもいいから
∃φ
追加だけでもいいか

**１３２人目の素数さん** · 2023/12/01(金) 15:27:11.98

>>98
基本的に暗号の問題は計算量
AIの今の問題は意味理解
根本的に問題が違う。形式化が意味するのは、数学の情報処理自体は可能ってこと

**１３２人目の素数さん** · 2023/12/01(金) 15:56:08.14

>>114
情報処理自体は可能
暗号は解くことが可能
可能であっても無意味ってことを喩えたのよ

**１３２人目の素数さん** · 2023/12/01(金) 15:56:50.02

まあええから
これくらいは解いて見せてほしいものだね
>>102

**１３２人目の素数さん** · 2023/12/01(金) 16:01:00.81

>>64
「探索アルゴリズム」があると思ってるのがまず噴飯モノ
それを>>70
>最初二行はふ～んという感じで無視するがw
そこがネックでしょ
さらに
譬えとして有限の「囲碁」を出してきてるのが次のコケどころ

**１３２人目の素数さん** · 2023/12/01(金) 16:05:15.87

>>117
>「探索アルゴリズム」があると思ってるのがまず噴飯モノ
普通の数学の問題を解けるくらいに有効な
は入れておくべきか
暗号だって探索アルゴリズムはあるはある

**１３２人目の素数さん** · 2023/12/01(金) 17:53:30.74

>>117
>>118
それらは俺は本質的な批判にならないと思ってるけど、その前に>>89は答えに
なってないと思う。集合論や圏論の一般論だけでは具体的な数学は出てこないって話
だよねと言ったら「底が浅い」と言うからその意味を聞いてるんだけど

改めて聞こう。一般論は具体的な理論と合わせなければ機能しないと言う話だ
それがどう底が浅い、基礎数学選書を読めという話になるのかを説明してくれ

**１３２人目の素数さん** · 2023/12/01(金) 18:02:16.85

>>119
知るつもりは無いみたいね

**１３２人目の素数さん** · 2023/12/01(金) 18:03:02.92

>>119
>本質的な批判にならないと思ってる
まあ
やって見せてから大言壮語するべきかと

**１３２人目の素数さん** · 2023/12/01(金) 18:04:28.16

>>119
>底が浅い
深い人は>>102は何かは分かってるのだろうか

**１３２人目の素数さん** · 2023/12/01(金) 18:16:14.32

>>120
根本的にずれてるね
「基礎数学を読むとこういうことがわかる、だから君は底が浅い」という具体的な
説明が必要だと言ってるんだけど
それができないのにただ読め、じゃ何の説得力も中身もない

74 １３２人目の素数さん 2023/11/30(木) 19:28:21.37 ID:afIXefRn
数学は集合論で全部できる
数学は論理学で全部できる
数学は圏論で全部できる
あと何でもイイヤ
全部展開できたからって
それで何が出てくるのかって話
使い古された言葉だけど
abstract nonsenseにならない方が
キモチイイと思うけどね

これをこっちは反復したわけで、それに底が浅いって言ってるのはブーメランでは？

**１３２人目の素数さん** · 2023/12/01(金) 18:22:53.42

>>123
ハイハイソノトオリデスワ

**１３２人目の素数さん** · 2023/12/01(金) 18:24:56.87

そもそも>>59
>LeanがLLMと融合したら9割の数学者はヤバいと、お前ら思わないのか？
これね
全然そんな感覚誰も持ってないと思うよってのを分かって貰えるかなと
起訴数学ぐらいは読んで欲しいと言ったわけ

**１３２人目の素数さん** · 2023/12/01(金) 18:25:28.12

ハイハイソノトオリデスワ

**１３２人目の素数さん** · 2023/12/01(金) 18:50:46.75

>>125
「誰も思ってない」という言い回しを使うのが逆に自信無さげに見えてしまう
8割の研究までは代替できそうと言ってる小山信也の例もあるわけだし、T.Taoは
GPTをもうすぐ研究パートナーくらいにはできそうだと言ってる
そしてAIの研究者はAGIを目指してるから、当然やるつもりでいる
GPTの五年前にも、誰もこれだけの成功を予想してなかった

とにかく客観的にはそういう状況だ

**１３２人目の素数さん** · 2023/12/01(金) 18:52:54.71

プログラミングは既にある程度できているわけだから、数学も普通に
考えたら危ないよ。証明はプログラムと同質なんだから

**１３２人目の素数さん** · 2023/12/01(金) 19:06:45.02

ハイハイソノトオリデスワ
ガンバッテネー
>>102ヨロシクー

**１３２人目の素数さん** · 2023/12/01(金) 19:08:14.84

>>127
>小山信也
誰よそれｗ
まあいいから
8割代替してから誇ってイイヨ
君は何も分かってないってよく分かった

**１３２人目の素数さん** · 2023/12/01(金) 19:08:39.76

分かる気が無いってことが分かった
か

**１３２人目の素数さん** · 2023/12/01(金) 19:11:08.32

もうちょっと言うと
キチンと理解して無いまま虎の威を借りようとしてるだけじゃないかなあ

**１３２人目の素数さん** · 2023/12/01(金) 19:12:07.19

数学者誰も虎の威とも思ってないけどね

**１３２人目の素数さん** · 2023/12/01(金) 19:15:31.11

>>128
>証明はプログラムと同質
カリーハワード同型対応持ち出すから
あーこの人は１＋１で暗号解いちゃう人だなって思われるのよ

**１３２人目の素数さん** · 2023/12/01(金) 19:20:28.22

たぶん
プログラムで云々は
仕様を与えてそれをプログラムしてくれるってやつでしょ
何処まで出来てるか知らないけど
「Mathematica作ってちょ」でマイMathematica作ってくれるんなら嬉しいね
今のところこれに関しても懐疑的ていうか眉唾
実際にやれてるところを見てみたいね

**１３２人目の素数さん** · 2023/12/01(金) 19:41:44.43

>>132
そっくりそのまま返すよ
可能性を否定してるだけで、数学わかってる奴特有の反論を全く見いだせない
数学者ならちゃんと論理的な理由を添えるけど、あんたのレスにはそれがない

**１３２人目の素数さん** · 2023/12/01(金) 19:44:54.24

まあ、どの辺を根拠に否定したがってるのかは大体わかりはするんだけどさ
でも数学をわかってる人間として反論するなら、もうちょい具体的にやってくれ
ないと、今んとこただの否定してる人だよね

**１３２人目の素数さん** · 2023/12/01(金) 19:50:08.24

>>134は良い反論ではあるのよ
確かにCH同型からだけでは、ただちにAIは数学者になるとは言えない
ただ、それが何を意味するのかを失礼ながらあんたは言語化できないらしい
もしAI研究者がそれを適切に言語化するならば、それが解ける可能性はあるね

誰だっけ？グロタンディークかキレンだったかが、適切な言語が見つかれば
問題は自然に解けると言った。AI研究も同じだろうね

**１３２人目の素数さん** · 2023/12/01(金) 19:54:29.84

なんか人の名前ばかりで語るだけで内容が全く感じられないんだが、こういうの詐欺師と見分けつかないし中身のある話をしろよ
なんかこの人の名前あげときゃいいだろみたいな態度が哲学みたいで気に入らない

**１３２人目の素数さん** · 2023/12/01(金) 19:56:58.61

やれるもんならやってみろ！

はその通りだと思うよ

**１３２人目の素数さん** · 2023/12/01(金) 19:58:20.32

実際にLEANやCoqやらで手を動かして苦労した経験とかがまるで感じられないんだよね
とりあえず数万行くらい証明を形式化した経験がないからこんな絵空事が言えるんだと思うよ

**１３２人目の素数さん** · 2023/12/01(金) 20:01:00.19

>>139
できそうな兆候はとっくに挙げてるけど
あんたが読めてないだけ
とりわけ、もしQ*アルゴリズムがGPTベースの自動推論で算数の問題を解けるなら、
数学でできない理由は何もない

**１３２人目の素数さん** · 2023/12/01(金) 20:06:09.97

>>141
それ全く反論になってなくない？
お前の体験談がないから無理に決まってると言ってるの？

**１３２人目の素数さん** · 2023/12/01(金) 20:07:21.26

>>142
それ算数じゃん

**１３２人目の素数さん** · 2023/12/01(金) 20:09:24.35

>>143
他人が研究してることをお前が偉そうに語るなって言ってんだよ
実際LEAN触ったことないんだろ？

**１３２人目の素数さん** · 2023/12/01(金) 20:14:57.64

「形式化は大変だ→これは絵空事だ」が全く繋がらないんだよね
形式化のデータが蓄積していて、膨大なデータから学習するのがLLMなんだが、
それが算数の問題を考えて解けるようになれば数学もできるのでは、というだけの話
それについて何をどう反論してるわけ？

むしろ躍起になって否定してるほうが今んとこ中身がないよ。あんたも含めて

**１３２人目の素数さん** · 2023/12/01(金) 20:17:57.81

>>145
だからそれ反論になってないじゃん
「具体的に」何が絵空事なのか言ってみ？あと偉そうなのは今んとこあんただよ
なら、お前もAIの研究者じゃないんだから俺らの話に気軽に口挟むなって返せるわ

**１３２人目の素数さん** · 2023/12/01(金) 20:21:34.30

>>142
算数ができて数学ができない理由は？自動推論は自動推論だろ
まともな反論もできないのに何偉そうにしてんの？

**１３２人目の素数さん** · 2023/12/01(金) 20:23:50.39

>>146
形式化の作業やったことないから蓄積してると考えちゃうんだよね
既存の形式化のメンテナンスやら、なんかミスったから最初から証明作り直さないとって世界なんたぞ

**１３２人目の素数さん** · 2023/12/01(金) 20:27:09.34

俺は予め「LLMの仕組みはまだよくわかってないがかなり上手くいってる」と
言ってるの理解してないな

つまり、展望はまだ不透明なわけよ
ところが自演かなんか知らねえが、アホが延々否定したがってる上に
お前Leanやってねえだろとか言い出したw
自演臭いけど、はっきり言って「できるかどうかわからないね」って素直に認めろよ
まともに否定する根拠を出せないならさ

**１３２人目の素数さん** · 2023/12/01(金) 20:28:59.87

>>149
論外だわ
とっくに機械学習の実験的適用始まってるの知らねえのかよ
そんなグチャグチャならやるわけないだろ
何のためにライブラリがあると思ってんだよ。オープンな再利用のためだぞ

**１３２人目の素数さん** · 2023/12/01(金) 20:30:18.57

こいつAIの研究してる人間だったのか
なんか算数できるAIを作った経験があって話してたのかな

**１３２人目の素数さん** · 2023/12/01(金) 20:30:49.83

>>149
要はコードの整合性取るの難しいって言いたいの？
そういうことをちゃんと言わないと何も伝わらんぞ

**１３２人目の素数さん** · 2023/12/01(金) 20:35:10.61

>>151
別にお前がやってるわけじゃないんだろ

**１３２人目の素数さん** · 2023/12/01(金) 20:35:42.46

大体Leanのトップを仕切ってる奴が、色んな形式化が蓄積してるし学部レベルなら
自動化できるようになるぜって言ってんだからそれはできるんだよ

あと「他人の発言使うな」とか言うのはマジで負けを認めてるようなもんだぞ
そんなこと言い出したらお前自力で証明してない数学の結果を一切使うなって話だ

**１３２人目の素数さん** · 2023/12/01(金) 20:37:40.36

>>154
幼稚園レベルだなお前。まずお前自身は何やってんだよ？
何にせよ、結局AIで数学やれない論拠を出せてないな

**１３２人目の素数さん** · 2023/12/01(金) 20:39:01.86

>>155
まだできてもない他人の仕事で、自分が関わってるわけでもないのに間違いなくできるとか言うのが不快だからやめろって言ってんだよ

**１３２人目の素数さん** · 2023/12/01(金) 20:39:39.64

>>156
そんなんあるわけないだろ

**１３２人目の素数さん** · 2023/12/01(金) 20:52:14.38

>>138
グロタンディークが言ったのは問題を適切に一般化すれば、かな
その適切な、というのがまさに問題だが

**１３２人目の素数さん** · 2023/12/01(金) 20:56:27.92

私はAIは問題の設定や概念の構築はできるようにならないと思っている
証明ならそれなりにできる様になるだろう
しかし証明も時には新しいフレームワークが必要になったりするしそういうレベルの問題は相当厳しいのではないか
意味のある問い、これをどうやって学習するのか？ビジョンや成功例があるのだろうか？

**１３２人目の素数さん** · 2023/12/01(金) 21:24:16.12

>>146
ハイハイソノトオリ

**１３２人目の素数さん** · 2023/12/01(金) 21:27:31.71

>>138
反論？アホか
呆れてるだけだわw
君には
>>102の命題が何であるかを答えて
その証明を書いた上で
それをプログラムにすることを要求するよw
大口叩いてるんだからそれくらいいいだろ？

**１３２人目の素数さん** · 2023/12/01(金) 21:29:48.78

>>160
>証明ならそれなりにできる様になるだろう
それなり」のレベルが問題よ
ほとんど役に立たないんじゃないかなあと思うけど
ちょっと驚くぐらいの証明をしてくれるんなら
数学者の友として役立つこともあるかもね

**１３２人目の素数さん** · 2023/12/01(金) 21:30:53.25

>>136
はぁ
ハイハイソノトオリ

**１３２人目の素数さん** · 2023/12/01(金) 21:33:09.51

嵐が多いみたいやね

**１３２人目の素数さん** · 2023/12/01(金) 21:46:15.20

君は数学も知らない上数学者も知らないようね

**１３２人目の素数さん** · 2023/12/01(金) 22:13:37.22

>>157
>>158
ちょっと丁寧に語ってやろうかと思ったけどやめた
できるもんはできるんだよ。ただこのスレでは俺は100%とは多分言ってないが

否定するより建設的な問いを立てたほうが役立つぞ
例えば「定理が美しい」とか「何か数学が面白い」といった表現がある
「これは手持ちの知識で証明できそうだな」とかな
そういう感覚表現には理由があるはずだ。これを理論的に解けるか？
神秘に閉じ込める奴は才能がないんだよ。後はまさにできるかどうか、ってだけだ

**１３２人目の素数さん** · 2023/12/01(金) 22:34:43.66

> ちょっと丁寧に語ってやろうかと思ったけどやめた

わろた

**１３２人目の素数さん** · 2023/12/01(金) 22:44:44.96

>>167
大口叩くだけ
表面なぞるだけ
証明の苦労も喜びも知らない
まともな数学書1冊ぐらい自分のものにしてみたらどう？

**１３２人目の素数さん** · 2023/12/01(金) 22:58:47.51

既存の証明を学習のソースにするにしても、LEANの証明スクリプトを食わせるのか、証明項を食わせてみるのか、型推論した型情報もいれるのか、自然言語の証明になんか翻訳して食わせるのか、どういうアイデアでうまくいきそうなのか是非語って欲しいわ

**１３２人目の素数さん** · 2023/12/02(土) 00:44:05.98

こっちでやれや

牛肉の数学
https://rio2016.5ch.net/test/read.cgi/math/1701433007/l50

**１３２人目の素数さん** · 2023/12/02(土) 00:53:44.17

定理：(X,d)はコンパクト距離空間で、f：X→X は写像で、
任意の異なる x,y∈X に対して d(f(x),f(y))＜d(x,y) が成り立つとする。
このとき、ただ1つの x∈X が存在して f(x)＝x が成り立つ。

この定理は不動点定理の一種であり、Edelstein によって証明されている。

**１３２人目の素数さん** · 2023/12/02(土) 00:55:55.93

仮定されている条件は、

・任意の異なるx,y∈Xに対して d(f(x),f(y))＜d(x,y)

でなければならず、不等号＜の部分を ≦ に変えて

・任意の異なるx,y∈Xに対して d(f(x),f(y))≦d(x,y)

に変更すると、反例が存在する。
つまり、＜なのか ≦ なのかという微妙な違いが大きな役割を果たしている。

**１３２人目の素数さん** · 2023/12/02(土) 00:59:53.99

>>172
それは明らかに成り立たんやろみたいな細かいチェックをせずにAIが間違った証明始めて人間が修正しろって突っ込んでも永遠に直らなさそう

**１３２人目の素数さん** · 2023/12/02(土) 01:01:12.53

この定理に関して、数学者がAIに期待する役割は
次のようなものであろう。

・「＜」という条件の場合には、
　定理が成り立つことをAIがちゃんと証明してくれる。

・「≦」という条件の場合には、
　定理が成り立たないことを反例つきでAIが指摘してくれる。

少なくとも現状のAIに、こんな芸当はできない。
そして、多くの数学はこのような微妙な差異の上に成り立っている。
その条件のときのみ奇跡的に定理が成り立ち、条件を僅かに変更したただけで
反例まみれになる、という綱渡りの上に数学の営みがある。

**１３２人目の素数さん** · 2023/12/02(土) 01:12:13.01

現状のAIが多少進化したところで、AIが出力する回答は
次のようなものになると思われる。

「＜」という条件の場合：
証明を出力するが、間違っている。間違いであることを
人間が指摘しても、依然として間違い続ける。
あるときには「反例がありました」などと言い出す。

「≦」という条件の場合：
証明を出力するが、そもそも反例があるので自動的に間違っている。
間違いであることを人間が指摘しても、別の証明を出力する。
もちろん反例があるので、自動的に間違っている。
やっと「反例がありました」と言い出しても、
その反例自体が間違っている。

**１３２人目の素数さん** · 2023/12/02(土) 01:18:20.51

そんなポンコツなAIであっても、必ずしも役に立たないわけではない。

・ AIが提示した証明が間違っていても、部分的なアイデアは
　正しい可能性がある。そこを数学者が拾い上げることで、
　数学者が正しい証明に到達できるかもしれない。

・ AIが提示した反例が間違っていても、反例の方向性自体は
　正しい可能性がある。そこを数学者が拾い上げることで、
　数学者が正しい反例を構築できるかもしれない。

このレベルのAIで実用的なものが登場する可能性はあるだろう。
しかし、それは数学者が仕事を失うことを意味しない。
それどころか、主体は依然として数学者である。

**１３２人目の素数さん** · 2023/12/02(土) 07:35:47.97

>>102
さらに訂正

∃φ,N,s,p,m,P,g(∀a(￢a∈φ)
　∧φ∈N
　∧s⊂N×N
　∧∀a∈N∃b∈N([a,b]∈s)
　∧∀a,b,c∈N([a,b],[a,c]∈s→b=c)
　∧∀a,b,c∈N([a,b],[c,b]∈s→a=c)
　∧∀a∈N(￢[a,φ]∈s)
　∧∀M⊂N(φ∈M
　　∧∀a∈M∃b∈M([a,b]∈s)
　　→M=N)
　∧p⊂N×N×N
　∧∀a,b∈N∃c∈N([a,b,c]∈p）
　∧∀a,b,c,d∈N([a,b,c],[a,b,d]∈p→c=d)
　∧∀a∈N([a,φ,a]∈p)
　∧∀a,b,c∈N∃d,e∈N([b,d],[c,e]∈s
　　∧([a,b,c]∈p→[a,d,e]∈p))
　∧m⊂N×N×N
　∧∀a,b∈N∃c∈N([a,b,c]∈m）
　∧∀a,b,c,d∈N([a,b,c],[a,b,d]∈m→c=d)
　∧∀a∈N([a,φ,φ]∈m)
　∧∀a,b,c∈N∃d,e∈N([b,d]∈s
　　∧[a,c,e]∈p
　　∧([a,b,c]∈m→[a,d,e]∈m))
　∧P⊂N
　∧∀a,b,q∈N(q∈P
　　↔︎(￢q=φ
　　∧￢[φ,q]∈s
　　∧([a,b,q]∈m→[φ,a]∈s∨[φ,b]∈s)))
　∧g⊂N×N
　∧∀a∈N([a,a]∈g)
　∧∀a,b∈N∃c∈N([a,c]∈s
　　∧([a,b]∈g→[c,b]∈g∧￢[b,c]∈g))
　∧∀n∈N(n≠φ
　　∧￢[φ,n]∈s
　　→∃q∈P∃k∈N([n,n,k]∈p
　　　∧￢[n,q]∈g
　　　∧￢[q,k]∈g)))

**１３２人目の素数さん** · 2023/12/02(土) 07:52:23.80

>>173
>反例が存在する
f(x)=xね
この反例を「論理的」に出してきてくれるかな
つまり
試行錯誤で無限の可能性の中から割り出してくれるか
あるいは
この反例は「唯一の」の部分に関するものだけど
「存在する」の部分に関する反例
すなわち
∀x∈X(f(x)≠x)
であるXとfとして
たとえば円周の回転とかを「論理的」に割り出せるかな
もちろん学習した知識の中にそれがあれば一発なんだけどそれではもっと別の条件についての反例を出してきてくれるとはあんまり期待できないしやはり「論理的」に割り出せるようでないと心許ない

**１３２人目の素数さん** · 2023/12/02(土) 09:57:58.35

>>179
詰まらん例を出すね
円周の回転ぐらいにしないか？

**１３２人目の素数さん** · 2023/12/02(土) 10:37:28.16

>>180
短絡的ねそれも書いてるが？

**１３２人目の素数さん** · 2023/12/02(土) 10:41:42.33

あと
詰まらんのは当たり前ってことで
本来すぐ思いつくべきこと
けどその反例をちゃんと出してきてくれるか
実際存在していないAIがどういう反応するか
想像しても仕方ないことではあるけれど
何もないところから適切な例
それも当たり前の例を出してくるものかなあ
まあどうでもいいか

**１３２人目の素数さん** · 2023/12/02(土) 11:50:52.75

>>179
>反例を「論理的」に出してきてくれるかな
>つまり試行錯誤で無限の可能性の中から割り出してくれるか
>あるいはこの反例は「唯一の」の部分に関するものだけど
>「存在する」の部分に関する反例(たとえば円周の回転とか)を
>「論理的」に割り出せるかな

『どうも東■田です』
「◆川です」
『なんか反例を”論理的”に出せるか、といってるけど』
「まず、任意の命題P(x1,…,xn)を満たす
　x1,…,xnが存在すると矛盾する場合
　その証明を見つけ出す方法はあります」
『え、あるんだ　知らんかった』
「一方、命題P(x1,…xn)を満たす
　x1,…,xnが存在する場合、
　その例を見つけ出す方法は存在しません」
『え？そうなの？なんか感覚的に逆っぽいけど』
「もし、そのような方法が存在するとすると、
　命題を前提した場合の無矛盾性証明ができることになりますが
　それはゲーデルの不完全性定理に反します
　正確には述語論理の充足可能性問題の決定不能性といいますけど」
『でもある例を具体的に示せば充足可能であることは示せるよね』
「もちろん、そうです
　命題論理の場合、命題論理式を充足させる論理値は
　見つけられますが、その手数が多項式時間だとは証明できてません
　一方、具体的な真偽値を示してそれが式を充足させることは
　多項式時間で確認できます
　もし、前者が多項式時間で可能ならNP＝Pということになります」
『なんと！そういうことなんだ』

**１３２人目の素数さん** · 2023/12/02(土) 18:53:34.62

そんなことよりXが空のときを最初に考えろよ