数学論文には正式な検証が必要です。これは通常、審判によって非公式に行われます。しかし、もしレフェリーの役割が定義や定理の定式化を綿密にチェックするだけに縮小されるような、より堅牢なLean 4の方法に頼ることができたらどうでしょうか?自動生成コードのコンパイルは証明証明書となります。これは、私がアリストテレスを@HarmonicMath年まで長期的に行ったことです。 設計図の準備を手伝ってくれた@PietroMonticoneと@llllvvuuに感謝します。ここでは、私の友人ステファン・バランチュクによるチェビシボフの可分性列に関する論文を完全に正確に自己形式化したものを示します。コードは約5000行の非常に非自明なリーンです。本論文の矛盾や空白をすべて修正し(委任された命題の証明も含む)、 私はこのような実験を一連の投稿し、初歩的整数論、組合せ論、解析学(Mathlibで扱うあらゆる分野)など数学の一部分野で、証明の妥当性の文書化が大きく変わる時期に近づいていることを証明します。今年は慌ただしい一年になりそうです!