11個の正方形の最適詰め込み問題、Lean 4での形式化と検証が完了

何が形式化されたか

公開されたのは、11個の単位正方形を最小の正方形に詰め込む問題（最適詰め込み問題）の最適性を、証明支援系Lean 4で完全に形式化したリポジトリである。形式化された定理は、正方形の向きが任意でよく、境界での接触が合法であり、内部が互いに素であるというモデルの下で成り立つ。公開されている定理文（ElevenSquare/Optimality.lean）とT03ソースツリーは、このリポジトリの以前のmainブランチから変更されていないと説明されている。

検証はEvolvingProgramsの実行環境で行われ、7,920個のローカルLeanモジュールすべてが受理されたと報告されている。最終監査ではadmissionがゼロであり、証明のソース、レシート、依存関係、公理の監査も通過したとされる。

最適な辺の長さ

最適な正方形の辺の長さTは、(6u+4)/(1+2u−u²)で与えられると記されている。ここでuは、5u⁸−10u⁷−2u⁶+14u⁵+12u⁴−6u³+2u²+2u−1=0の(9/25, 37/100)区間における唯一の根である。この構成が達成する値は約3.8770835900228141773と示されている。

検証の信頼モデル

この形式化では、幾何、チェッカーの健全性、証明の組み立ては通常のLean証明で構成されている。一方、高コストで厳密な数値証明書のチェックの一部にはnative_decideが使われている。そのため最終定理が信頼するのはLeanのカーネルとネイティブコンパイラであり、「カーネルだけで検証した」という主張ではない点が明記されている。承認された数値宣言とそのソースハッシュはverification/native-certificates.jsonに記録されている。

再現手順と注意点

再現にはLean 4.34.1とMathlibのリビジョンd13f23b723b8a846827a245b89c10fc7d3f11612が固定されており、lake-manifest.jsonを変更しないことが求められる。LinuxまたはmacOSでスクリプトを実行し、オプションを付けると完全に再実行できる。検証成功の条件はOPTIMALITY_PROVED_WITH_NATIVE_CERTIFICATES、admissionゼロ、trust_model: lean_kernel_and_native_compilerであり、コンパイル済みモジュールが100%に達しただけでは不十分とされている。

なお、ソースのみのチェックは別のスクリプトで行える。成功した実行はEvolvingProgramsのより大きなランナーを用いたもので、コールドビルドの実行時間やmacOSでの2〜3時間という保証を示すものではないと注意されている。このスナップショットでは、過去のmaterializationコマンドやverify.py --setupを実行しないよう指示されている。