21/12/28 13:16:46.24 1vdB6O4M.net
>>193
過去スレでもIUT一派(世界的な数学界で公認された用語w)に動きがある時と
核心部の話になる時にはスレが場違いの話か理解不足の罵倒でスレがあれて
きたからスルーしながら、。
さて、
computer利用の証明の形式化より
IUT論文でIUTTの位置づけ問題点の
核心部が明確になり>>84さんが
貼ったBuzzardのpaperは重要で
しょう。加えて
・Formalising perfectoid spaces
arxiv 1910.12320
>Perfectoid spaces are sophisticated objects in arithmetic geometry introduced by Peter Scholze in 2012. We formalised enough definitions and theorems in topology, algebra and geometry to define perfectoid spaces in the Lean theorem prover.
Scholzeのperfect spaceは元々
数学の論文が洗練され明確だから
形式化の中で更に洗練されLeanに
対応できたでしょう
・Schemes in Lean
arxiv 2101.02602
> story of how schemes were formalised in three different ways
in the Lean theorem prover.
定義は3あり当然伝統的な層圏アフィンスキーム.ハーツホーン本もベース
にある。
またThe Stacks Projectが専門家に
高く評価されている。
IU幾何の構想はSchemeの拡張だけど
過去スレにあるようにここから
不明確と思う。