ここでは、最近の数学のレポートを完全に自己定式化したものを(またしても!)紹介します。 バランチュク、ステファン。「有限体上のn空間の部分集合を定義する方程式の数を減らす」トゥールーズ科学部年報:Mathématiques、シリーズ6、第33巻、第1号(2024年):177–182。 このプロジェクトに数日かけました。まず、アリストテレスを@HarmonicMathで解析し、約15時間で証明を完全に自動形式化しました。そして、@PietroMonticoneの大きな助けを借りて、証明の設計図版を作成することができました。このバージョンでは、LaTeXのすべてのドキュメントがインタラクティブになり、検査や学習が可能です。証明の依存関係を見て、それらの関係を研究することができます。 後処理段階では、Grok HeavyとCodex CLIを使い、xhighモードのGPT-5.2を使って形式証明の行ごとの分析を書きました。これは、プロのLean 4プログラマーでない人にとって非常に役立ちます。証明のすべてのステップを本当に内面化できます。 この経験から得た印象と学んだことをまとめたいと思います。@vladtenev @Leonard41111588 @HarmonicMath @llllvvuu @littmath @AlexKontorovich @jdlichtman @KenOno691 @CarinaLHong @gdb @hongyuan_mei