[過去ﾛｸﾞ] なぜ、ZFC公理まで遡らなくても数学が出来るの？ (1002ﾚｽ)
上下前次1-新

---

このｽﾚｯﾄﾞは過去ﾛｸﾞ倉庫に格納されています｡
次ｽﾚ検索 歴削→次ｽﾚ 栞削→次ｽﾚ 過去ﾛｸﾞﾒﾆｭｰ

---

94: 現代数学の系譜 雑談 ◆yH25M02vWFhP 2024/11/19(火)21:17 ID:/e7NmevV(2/3) AA×


[240|320|480|600|100%|JPG|べ|ﾚｽ栞|ﾚｽ消]
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
つづき コンピュータが定理を証明するというこのようなシステム では対話的に人間とコンピュータが入力出力をかわしながら証明を構築していくらしいですこういうのはなどが得意とする作業なのでとを組み合わせて定理を証明していくというシステムも研究されているとのことでしたについてもうすこし知りたくなりますね このについての講習会が日本で去年あったそうでその資料が公表されていますのインストールの仕方の動画などもあるのでインストールして遊んでみるのもよいかもと思います 数学系のための勉強会 つづく

---

上下前次1-新書関写板覧索設栞歴

---

あと 908 ﾚｽあります
ｽﾚ情報 赤ﾚｽ抽出 画像ﾚｽ抽出 歴の未読ｽﾚ AAｻﾑﾈｲﾙ

---

ぬこの手 ぬこTOP 0.032s