[過去ﾛｸﾞ]
Inter-universal geometry と ABC 予想 46 (1002ﾚｽ)
上
下
前
次
1-
新
このｽﾚｯﾄﾞは過去ﾛｸﾞ倉庫に格納されています｡
次ｽﾚ検索
歴削→次ｽﾚ
栞削→次ｽﾚ
過去ﾛｸﾞﾒﾆｭｰ
146
: 2020/04/05(日)00:13
ID:X6bu6ndd(1)
AA×
>>70
[
240
|
320
|480|
600
|
100%
|
JPG
|
べ
|
ﾚｽ栞
|
ﾚｽ消
]
146: [sage] 2020/04/05(日) 00:13:21 ID:X6bu6ndd >>70 > 最初っからこの件で良く分からないのは、数学ってそんなに分かりにくい学問だったっけかってことなんだよな > ステップごとには論理式で書けるような内容であるはずで、長いっても1000ページ切ってるんだろ あのなあ、600ページの論文を本当にガチガチの論理式で書き直す、つまりCoqなどの証明チェッカで証明に抜けがないか 完全にチェック可能なように形式化したら、その論文が前提としている既存の数学理論の形式化のサイズは含まずに その論文自身の定義や各種の命題のステートメントやそれらの証明の形式化のサイズだけでも元の論文のサイズの軽く100倍以上になるぞ 一流の数学者が定理の証明のある部分を「明らか」の一言で済ませている時に、その部分を形式化して完全に基本推論規則の積み重ねに 書き直して抜けがないようにするだけで数百行になるケースは決して珍しくない > ある程度素養のある人が眺めてみて何が本質的なアイデアか全くわからないなんてことがあり得るのかね？ 十分に有り得る 恐らくショルツは望月のIUTで定義している様々な概念のイメージを頭の中で正しく組み立てられないと推測される http://rio2016.5ch.net/test/read.cgi/math/1585967607/146
最初っからこの件で良く分からないのは数学ってそんなに分かりにくい学問だったっけかってことなんだよな ステップごとには論理式で書けるような内容であるはずで長いってもページ切ってるんだろ あのなあページの論文を本当にガチガチの論理式で書き直すつまりなどの証明チェッカで証明に抜けがないか 完全にチェック可能なように形式化したらその論文が前提としている既存の数学理論の形式化のサイズは含まずに その論文自身の定義や各種の命題のステートメントやそれらの証明の形式化のサイズだけでも元の論文のサイズの軽く倍以上になるぞ 一流の数学者が定理の証明のある部分を明らかの一言で済ませている時にその部分を形式化して完全に基本推論規則の積み重ねに 書き直して抜けがないようにするだけで数百行になるケースは決して珍しくない ある程度素養のある人が眺めてみて何が本質的なアイデアか全くわからないなんてことがあり得るのかね？ 十分に有り得る 恐らくショルツは望月ので定義している様な概念のイメージを頭の中で正しく組み立てられないと推測される
上
下
前
次
1-
新
書
関
写
板
覧
索
設
栞
歴
あと 856 ﾚｽあります
ｽﾚ情報
赤ﾚｽ抽出
画像ﾚｽ抽出
歴の未読ｽﾚ
AAｻﾑﾈｲﾙ
ぬこの手
ぬこTOP
0.047s