[過去ﾛｸﾞ] なぜ、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
野村一也 「科学を学ぶ人のために」 九大野村研ホームページの拡張版です
コンピュータが数学の定理を自動的に証明する!!？
投稿日: 2024年10月19日 投稿者: root
以前、講習会で九大の溝口 佳寛先生による、コンピュータによる定理証明支援系 Coqのお話を聞いたことを書きました。最近、 Coq とは別の証明支援系（theorem prover）である、Leanというのが特に話題になっています。Coqはより以前から開発されているシステムですが、Leanは後発でそれなりに強力なシステムのようです。たとえば雑誌『数学セミナー』の2024年8月号（特集 「生成AIとこれからの数学」）によると、フィールズ賞受賞者のショルツェが構築したCondensed Mathematicsのある定理の証明の正しさの検証にLeanが用いられ、他の数学者に先駆けて検証に成功したとのことです。またLeanを用いてフェルマーの定理の証明を行う試みがあるというのもこの号の記事で知りました。きっと京大の望月新一先生によるABC予想の証明の検証も こうしたコンピュータによる証明支援系を使って行えるのではなかろうか、などと妄想しているところです。
つづく
上下前次1-新書関写板覧索設栞歴
あと 909 ﾚｽあります
ｽﾚ情報 赤ﾚｽ抽出 画像ﾚｽ抽出 歴の未読ｽﾚ AAｻﾑﾈｲﾙ
ぬこの手 ぬこTOP 0.008s