[過去ﾛｸﾞ]
なぜ、ZFC公理まで遡らなくても数学が出来るの？ (1002ﾚｽ)
なぜ、ZFC公理まで遡らなくても数学が出来るの？ http://rio2016.5ch.net/test/read.cgi/math/1731415731/
上
下
前次
1-
新
通常表示
512ﾊﾞｲﾄ分割
ﾚｽ栞
抽出解除
必死ﾁｪｯｶｰ(本家)
(べ)
自ID
ﾚｽ栞
あぼーん
このｽﾚｯﾄﾞは過去ﾛｸﾞ倉庫に格納されています｡
次ｽﾚ検索
歴削→次ｽﾚ
栞削→次ｽﾚ
過去ﾛｸﾞﾒﾆｭｰ
93: 現代数学の系譜 雑談 ◆yH25M02vWFhP [] 2024/11/19(火) 21:15:34.69 ID:/e7NmevV >>92 ご苦労さまです ID:yXKQG6fo は、おサルの お連れ かｗ ；ｐ）（http://rio2016.5ch.net/test/read.cgi/math/1731325608/155 ） いまどき >>1 ZFC公理なんて オワコンでしょ？ いまどきトレンドは、下記かもねｗ ；ｐ） ホイヨ！ glycostationx.org/2024/10/19/ The Nomura Institute of Glycosciece Blog 野村一也 「科学を学ぶ人のために」 九大野村研ホームページの拡張版です コンピュータが数学の定理を自動的に証明する!!？ 投稿日: 2024年10月19日 投稿者: root 以前、講習会で九大の溝口 佳寛先生による、コンピュータによる定理証明支援系 Coqのお話を聞いたことを書きました。最近、 Coq とは別の証明支援系（theorem prover）である、Leanというのが特に話題になっています。Coqはより以前から開発されているシステムですが、Leanは後発でそれなりに強力なシステムのようです。たとえば雑誌『数学セミナー』の2024年8月号（特集 「生成AIとこれからの数学」）によると、フィールズ賞受賞者のショルツェが構築したCondensed Mathematicsのある定理の証明の正しさの検証にLeanが用いられ、他の数学者に先駆けて検証に成功したとのことです。またLeanを用いてフェルマーの定理の証明を行う試みがあるというのもこの号の記事で知りました。きっと京大の望月新一先生によるABC予想の証明の検証も こうしたコンピュータによる証明支援系を使って行えるのではなかろうか、などと妄想しているところです。 つづく http://rio2016.5ch.net/test/read.cgi/math/1731415731/93
94: 現代数学の系譜 雑談 ◆yH25M02vWFhP [] 2024/11/19(火) 21:17:21.15 ID:/e7NmevV つづき コンピュータが定理を証明するというこのようなシステム＝theorem proverでは対話的に人間とコンピュータが入力・出力をかわしながら証明を構築していくらしいです。こういうのはChatGPTなどが得意とする作業なので、ChatGPTとLeanを組み合わせて定理を証明していくというシステムも研究されているとのことでした。Leanについてもうすこし知りたくなりますね。 このLeanについての講習会が日本で去年あったそうで、その資料が公表されています。Leanのインストールの仕方の動画などもあるので、インストールして遊んでみるのもよいかもと思います。 【数学系のためのLean勉強会 Lean for math workshop】 haruhisa-enomoto.github.io/lean-math-workshop/ つづく http://rio2016.5ch.net/test/read.cgi/math/1731415731/94
95: 現代数学の系譜 雑談 ◆yH25M02vWFhP [] 2024/11/19(火) 21:17:49.45 ID:/e7NmevV つづき 教材はこちらにあります。 github.com/yuma-mizuno/lean-math-workshop インストール動画を埋め込んでおきます。 【定理証明支援系Leanの始め方講座（Windows編）【VOICEROID解説】】 youtu.be/LDfmNmzY5_8?si=_z0sOy2zFPIIHx5g (引用終り) 以上 http://rio2016.5ch.net/test/read.cgi/math/1731415731/95
ﾒﾓ帳
(0/65535文字)
上
下
前次
1-
新
書
関
写
板
覧
索
設
栞
歴
ｽﾚ情報
赤ﾚｽ抽出
画像ﾚｽ抽出
歴の未読ｽﾚ
AAｻﾑﾈｲﾙ
Google検索
Wikipedia
ぬこの手
ぬこTOP
0.183s*