>>97-98
どうもです
ID:yRMZ8PCLは、ヒキコモリ数学基礎論くんか
今年もよろしくお願いいたします。

さて、
>加藤先生はNスペでも言ってたけどiutがleanを通せるような現代数学の言語で記述できると思っていない
>なのでやらんやろ

これは、（下記）>>78 新一ブログ からの抜粋関連 ですね
「Leanによる形式化は、長期的な検証や説明責任を可能にする記録装置となり得るか？」
（関連記述）
”私自身はこれまでそういう計算機のプログラミングの世界とは全く縁がなかったですし、今でも私自身が直接プログラムのコードを書く立場ではなく、専門家がコードを書けるように、数学的な理論の整理の仕組みを考え直したりして、関連した資料の作成やメール上の議論を通して数学側からコードを書く業務のお手伝いをする立場です。つまり、これまでのように、人間の数学者ではなく、（直接コードを書く立場の専門家を介して）いわば計算機を相手に自分の研究を解説することによって様々な新たな数学的知見を獲得する機会に恵まれ、数学者としても非常に有意義な刺激を得ているということです。”

さて、上記で浮かぶ疑問
１）”直接コードを書く立場の専門家”なる 非数学者＝職人さん を雇って Leanプログラムを書いてもらう と読める
２）では、職人さん を雇う予算が どこから出ているのか？
　おそらくは、下記の ZMCの予算でしょう
３）思うに、職人さんは一人かも。そして、望月氏は ドカと資料を渡して 読めと言って
　あとは メール上の議論で 質問が来ると回答 その繰返し

なので、ここには 加藤先生は 非介在ですね　（＾＾

(参考)
https://zen.ac.jp/zmc/topics/j9oxyiomf
2025.02.20
Conference Name: ZMC Conference 2025
Title: Anabelian Geometry and its Computer Formalization
Dates: July 1 - July 4, 2025
Conference Theme:
Recently, more and more people have become interested in the formalization of mathematics by computers, and are becoming more and more aware that Lean4 formalizations and verifications of mathematics have the potential to significantly change the way of doing the research mathematics in the future.