Inter-universal geometry と ABC予想 (応援スレ) 74 (963ﾚｽ)
上下前次1-新
抽出解除 ﾚｽ栞

---

ﾘﾛｰﾄﾞ規制です｡10分ほどで解除するので､他のﾌﾞﾗｳｻﾞへ避難してください｡

---

307(1): 現代数学の系譜 雑談 ◆yH25M02vWFhP 08/26(火)21:01 ID:dSyweoWi(2/4) AAS
つづき

形式化された理論
メンタルピクチャーの対極にあるのは、形式化（formalize）されコード化された理論（FT）だ。
数学の研究論文における形式的●●●議論は、例えばLean4やCoqなどのコンピューター言語による形式化からすれば、まだまだ「非形式的（informal）」なものだろう。人間のやる数学はまだまだインフォーマルであり、行間が広く、とてもとても形式的議論とは言えない。
とはいえ、ここで「メンタルピクチャー（MP）」の対極にある概念としての「形式化された理論（FT）」は、人間の書いた論文の議論のようなものも含む、広い概念である。そして、数学の厳密化とか精密化とは、このような緩い意味での形式化
(*)　　MP ーーーー形式化ー＞ FT
のことである。
省10

---

311(2): 08/26(火)22:59 ID:v2xfVefA(20/23) AAS
>>306-307
君、なんとかピクチャー大好きだね
でも無意味だね
だって君、口を開けば間違いだらけじゃん　なんとかピクチャー全然役に立ってないじゃん

---

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

---

ｽﾚ情報 赤ﾚｽ抽出 画像ﾚｽ抽出 歴の未読ｽﾚ AAｻﾑﾈｲﾙ

---

ぬこの手 ぬこTOP 0.030s