>>531
>証明論に限らず数学の形式化が進んでるから
>昔みたいなことはもう起きないよ

たぶん 違うんじゃ無いかな
１）まず、下記の 渕野先生が書いている
”厳密性を数学と取りちがえるという勘違い”
２）さらには、形式化の限界
　これは、下記ゲーデル不完全性定理の話（下記）
　”証明できない真実: 第一不完全性定理により、内容としては正しい（真である）にもかかわらず、その体系の中のルール（公理）だけでは「正しい」と証明できない命題が必ず存在することが示されました”

要するに、数学とは IUTのLean形式化の失敗をのり超えて 進んでいくものだと思う
（それは、何かを追加して Lean形式化が出来るのか 逆に IUTは根本に問題あり となるか どちらか不明だが）

(google検索)
ゲーデル不完全性定理の数学における意義は何か？
AI による概要
ゲーデルの不完全性定理の数学における意義は、「すべての数学の真理を完全に証明できる一つの完璧なルールブック（公理系）を作ることはできない」と示したことです。主な意義として、ヒルベルト・プログラムの挫折、真と証明の乖離、数学基礎論の発展があげられます
ヒルベルト・プログラムの挫折
略
「真理」と「証明」の限界
・証明できない真実: 第一不完全性定理により、内容としては正しい（真である）にもかかわらず、その体系の中のルール（公理）だけでは「正しい」と証明できない命題が必ず存在することが示されました

　>>30より再録
＜厳密だけが、数学ではない＞
＜数学と厳密＞
あなたのまったく逆を、渕野先生が書いている
”厳密性を数学と取りちがえるという勘違い”
https://www.amazon.co.jp/dp/4480095470
数とは何かそして何であるべきか デデキント 訳解説 渕野昌 筑摩書房2013
「数学的直観と数学の基礎付け 訳者による解説とあとがき」
P314
(抜粋)
数学の基礎付けの研究は，数学が厳密でありさえすればよい， という価値観を確立しようとしているものではない.
これは自明のことのようにも思えるが，厳密性を数学と取りちがえるという勘違いは，
たとえば数学教育などで蔓延している可能性もあるので，
ここに明言しておく必要があるように思える
多くの数学の研究者にとっては，数学は，記号列として記述された「死んだ」数学ではなく，
思考のプロセスとしての脳髄の生理現象そのものであろう
したがって，数学はその意味での実存として数学者の生の隣り合わせにあるもの，と意識されることになるだろう
そのような「生きた」「実存としての」(existentialな)数学で問題になるのは，
アイデアの飛翔をうながす(可能性を持つ)数学的直観」とよばれるもので，
これは， ときには，意識的に厳密には間違っている議論すら含んでいたり，
寓話的であったりすることですらあるような，
かなり得体の知れないものである