なぜ、ZFC公理まで遡らなくても数学が出来るの？ (123ﾚｽ)
上下前次1-新

---

93(1): 現代数学の系譜 雑談 ◆yH25M02vWFhP 11/19(火)21:15 ID:/e7NmevV(1/3) AA×
>>92>>1

ID:yXKQG6fo
2chｽﾚ:math

[240|320|480|600|100%|JPG|べ|ﾚｽ栞|ﾚｽ消]
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
ご苦労さまです はおサルの お連れ か いまどき 公理なんて オワコンでしょ？ いまどきトレンドは下記かもね ホイヨ！ 野村一也 科学を学ぶ人のために 九大野村研ホームページの拡張版です コンピュータが数学の定理を自動的に証明する？ 投稿日 年月日 投稿者 以前講習会で九大の溝口 佳寛先生によるコンピュータによる定理証明支援系 のお話を聞いたことを書きました最近 とは別の証明支援系 であるというのが特に話題になっていますはより以前から開発されているシステムですがは後発でそれなりに強力なシステムのようですたとえば雑誌数学セミナーの年月号特集 生成とこれからの数学によるとフィールズ賞受賞者のショルツェが構築した のある定理の証明の正しさの検証にが用いられ他の数学者に先駆けて検証に成功したとのことですまたを用いてフェルマーの定理の証明を行う試みがあるというのもこの号の記事で知りましたきっと京大の望月新一先生による予想の証明の検証も こうしたコンピュータによる証明支援系を使って行えるのではなかろうかなどと妄想しているところです つづく

---

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

---

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

---

ぬこの手 ぬこTOP 0.037s