AI支援による11個の正方形の最適パッキング証明

Leanにおける11個の正方形のパッキング 最適性証明は、ネイティブ数値証明書によって検証されました。完了したEvolvingProgramsの検証実行は、7,920個全てのローカルLeanモジュールを受け入れ、最終監査ではゼロの誤りを報告しました。このリポジトリは、コミット1bf942a7af1ea330e95489d8997deebd4227ca71からの正確な証明ソースとピン留めされたビルド構成をインポートします。証拠と範囲については、検証レポートを参照してください。 選択された計算コストの高い正確な数値証明書のチェックにはnative_decideを使用します。ジオメトリ、チェッカーの健全性、および証明のアセンブリは、通常のLean証明を維持します。したがって、最終定理はLeanのカーネルとネイティブコンパイラを信頼します。これはカーネルのみの検証主張ではありません。承認された数値宣言とその正確なソースハッシュは、verification/native-certificates.jsonに記録されています。 最適辺長は T = (6u+4)/(1+2u-u^2) です。ここで、uは 5u^8-10u^7-2u^6+14u^5+12u^4-6u^3+2u^2+2u-1=0 の(9/25, 37/100)における唯一の根です。この構成は、約3.8770835900228141773を達成します。モデルは、任意の向き、合法的な境界接触、および互いに素な開いた内部を許可します。ElevenSquare/Optimality.leanの公開ステートメントと、完全なT03ソースツリーは、このリポジトリの以前のメインブランチから変更されていません。 エントリポイント ファイル 目的 ElevenSquare/Foundations.lean ジオメトリ、正確な終点、達成構成、閉じたセルカバー、および有限ケースの削減。 ElevenSquare/Pending/ 元の公開インターフェース。現在は統合された証明によって処理されています。ディレクトリ名は歴史的なものです。 ElevenSquare/Interop/Wand125/ 組み込まれた上流証明書の結果への接続。 ElevenSquare/Tasks/ 幾何学的引数、チェッカー、証明書データ、およびローカル解析証明。 Sqpack/ 組み込まれた証明書チェッカー、生成された証明、および簡略化。 ElevenSquare/Optimality.lean 無条件の最適性および辺長下限定理。 ElevenSquare/Verification.lean 公開証明ターゲットのアクシヨムクエリ。 検証の再現 プロジェクトはLean 4.34.1とMathlibリビジョンd13f23b723b8a846827a245b89c10fc7d3f11612をピン留めしています。lake-manifest.jsonは変更しないでください。 LinuxでPython 3、Git、curl、およびtarを使用する場合：bash scripts/run_verification.sh --bootstrap --jobs 2 macOSでは、まずelanランチャーをインストールしてから、同じコマンドを使用してください。elanが既にインストールされている場合、ブートストラップはピン留めされたツールチェーンと依存関係キャッシュを準備できます。マシンに適したワーカー数を選択してください。モジュールはシリアルにコンパイルされます。既存の有効なレシートは再利用可能です。 完全な再実行を強制するには--freshを追加してください。Ctrl-Cはランナーをクリーンに停止します。コマンドは、全てのローカルモジュールをチェックし、最終的なソース、レシート、依存関係、およびアクシヨム監査を実行します。最終結果で、OPTIMALITY_PROVED_WITH_NATIVE_CERTIFICATES、ゼロの誤り、およびtrust_model: lean_kernel_and_native_compilerを要求します。コンパイルされたモジュールの100%に到達しただけでは十分ではありません。 ソースのみのチェック（Leanなし）は次のとおりです：python3 scripts/check_sources.py 手動ワークフローとUbuntuの手順も、再開可能な検証をサポートしています。プッシュはワークフローを開始しません。成功したソース実行はEvolvingProgramsのより大きなランナーを使用しました。これはコールドビルドの実行時間や2〜3時間のmacOS保証を確立するものではありません。このスナップショットで、歴史的なマテリアライゼーションコマンドやverify.py --setupを実行しないでください。それらは置き換えられた生成ソースを復元します。ビルドオブジェクトとログは、無視される.lake/および.verification/ディレクトリに属します。 クレジットと出所 EvolvingPrograms、@ctjlewis、および全てのプロジェクト貢献者に、フォーマル化と検証作業に感謝します。個々の貢献者および上流のクレジットについてはACKNOWLEDGEMENTS.mdを、ソース履歴についてはPROVENANCE.mdを、保持された通知についてはintegrations/wand125を参照してください。歴史的な簡略化ノートと部分的な監査記録は保持されています。それらの古い未完了ステートメントは、完了した実行レポートによって置き換えられています。