パーフェクトイド空間

バザード、コメリン、マソット著

パーフェクトイド空間は2012年にピーター・ショルツによって導入された、数論幾何学における洗練された対象である。
我々はLean定理証明器でパーフェクトイド空間を定義するのに十分な.位相幾何学.代数学.幾何学における定義と定理を形式化した。
この実験は、証明支援システムが単純な対象に関する長い証明を形式化することとはかなり異なる、その方向性の複雑さを扱うことができることを確認している