なぜ、ZFC公理まで遡らなくても数学が出来るの? (123レス)
なぜ、ZFC公理まで遡らなくても数学が出来るの? http://rio2016.5ch.net/test/read.cgi/math/1731415731/
上
下
前
次
1-
新
通常表示
512バイト分割
レス栞
93: 現代数学の系譜 雑談 ◆yH25M02vWFhP [] 2024/11/19(火) 21:15:34.69 ID:/e7NmevV >>92 ご苦労さまです ID:yXKQG6fo は、おサルの お連れ かw ;p)(http://rio2016.5ch.net/test/read.cgi/math/1731325608/155 ) いまどき >>1 ZFC公理なんて オワコンでしょ? いまどきトレンドは、下記かもねw ;p) ホイヨ! 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サムネイル
Google検索
Wikipedia
ぬこの手
ぬこTOP
0.003s