[過去ﾛｸﾞ] なぜ、ZFC公理まで遡らなくても数学が出来るの？ (1002ﾚｽ)
上下前次1-新
抽出解除 必死ﾁｪｯｶｰ(本家) (べ) ﾚｽ栞 あぼーん
このｽﾚｯﾄﾞは過去ﾛｸﾞ倉庫に格納されています｡
次ｽﾚ検索 歴削→次ｽﾚ 栞削→次ｽﾚ 過去ﾛｸﾞﾒﾆｭｰ
93(1): 現代数学の系譜 雑談 ◆yH25M02vWFhP 2024/11/19(火)21:15 ID:/e7NmevV(1/3) AAS
>>92
ご苦労さまです
ID:yXKQG6fo は、おサルの お連れ かｗ ；ｐ）（2chｽﾚ:math ）
いまどき >>1 ZFC公理なんて オワコンでしょ？
いまどきトレンドは、下記かもねｗ ；ｐ）
ホイヨ！
glycostationx.org/2024/10/19/
The Nomura Institute of Glycosciece Blog
野村一也 「科学を学ぶ人のために」 九大野村研ホームページの拡張版です
コンピュータが数学の定理を自動的に証明する!!？
省3
94: 現代数学の系譜 雑談 ◆yH25M02vWFhP 2024/11/19(火)21:17 ID:/e7NmevV(2/3) AAS
つづき
コンピュータが定理を証明するというこのようなシステム＝theorem proverでは対話的に人間とコンピュータが入力・出力をかわしながら証明を構築していくらしいです。こういうのはChatGPTなどが得意とする作業なので、ChatGPTとLeanを組み合わせて定理を証明していくというシステムも研究されているとのことでした。Leanについてもうすこし知りたくなりますね。
このLeanについての講習会が日本で去年あったそうで、その資料が公表されています。Leanのインストールの仕方の動画などもあるので、インストールして遊んでみるのもよいかもと思います。
【数学系のためのLean勉強会 Lean for math workshop】
haruhisa-enomoto.github.io/lean-math-workshop/
つづく
95: 現代数学の系譜 雑談 ◆yH25M02vWFhP 2024/11/19(火)21:17 ID:/e7NmevV(3/3) AAS
つづき
教材はこちらにあります。
github.com/yuma-mizuno/lean-math-workshop
インストール動画を埋め込んでおきます。
【定理証明支援系Leanの始め方講座（Windows編）【VOICEROID解説】】
youtu.be/LDfmNmzY5_8?si=_z0sOy2zFPIIHx5g
(引用終り)
以上
上下前次1-新書関写板覧索設栞歴
ｽﾚ情報 赤ﾚｽ抽出 画像ﾚｽ抽出 歴の未読ｽﾚ AAｻﾑﾈｲﾙ
ぬこの手 ぬこTOP 1.808s*