>>654
(引用開始)
加藤文元さんの語り、面白い （＾＾
https://youtu.be/b6JlM_nrM3M?t=1
【ReHacQ生配信】AIで数学を証明!?IUT理論は正しいのか【高橋弘樹vs川上量生vs野村泰紀vs加藤文元】
ReHacQ−リハック−【公式】
166,727回視聴 2026/07/24
(引用終り)

これで、加藤文元が動画中で紹介していた ショルツェ氏の話が
下記
Liquid Tensor Experiment
”2020年、ショルツェは、液体ベクトル空間の概念を用いて、関数解析と複素幾何学を凝縮数学の枠組みに組み込むことを可能にする結果の証明を完成させた”
”彼は他の数学者に形式化され検証された証明を提供するよう依頼した”
”ヨハン・コメリン率いるグループが証明支援ツールLeanを使用して証明の中央部分を検証した”
だね
ふむふむ

(参考)
https://leanprover-community.github.io/blog/posts/lte-final/
Lean community blog
Completion of the Liquid Tensor Experiment
Mathlib community 2022-07-15

We are proud to announce that as of 15:46:13 (EST) on Thursday, July 14 2022 the Liquid Tensor Experiment has been completed. A year and a half after the challenge was posed by Peter Scholze we have finally formally verified the main theorem of liquid vector spaces using the Lean proof assistant. The blueprint for the project can be found here and the formalization itself is available on GitHub.

The first major milestone was announced in June last year. The achievement was described in Nature and Quanta.

For more information about Lean and formalization of mathematics, see the Lean community website.

Statement
略

https://en.wikipedia.org/wiki/Condensed_mathematics
Condensed mathematics
History
(google訳)
2020年、ショルツェは、液体ベクトル空間の概念を用いて、関数解析と複素幾何学を凝縮数学の枠組みに組み込むことを可能にする結果の証明を完成させた。議論は非常に微妙であることが判明し、結果の妥当性に関する疑念を払拭するために、彼は他の数学者に形式化され検証された証明を提供するよう依頼した。[ 6 ] [ 7 ] 6か月にわたり、ヨハン・コメリン率いるグループが証明支援ツールLeanを使用して証明の中央部分を検証した。[ 8 ] [ 7 ] 2022年7月14日現在、証明は完了している。[ 9 ]