Leanが11正方形詰め込み問題の最適性を証明、7920モジュールを検証
AI-assisted proof of optimal packing for 11 squares
11個の正方形を最小の正方形に詰め込む最適性の完全な証明がLeanで形式化され、7920のローカルモジュールが検証に合格した。ネイティブ数値証明書を用いた検証では、最終定理はLeanカーネルとネイティブコンパイラのみを信頼する。最適辺長はuの8次方程式の根で与えられ、約3.8770835900228141773に達する。
最終定理はLeanのカーネルとネイティブコンパイラを信頼する。これはカーネルのみの検証主張ではない。
HNでの議論
48- golden-face
正方形詰め込みが実際に何を意味するのか理解するのにちょっと時間がかかった（Wikiが参考になる）が、要するに：単位正方形（1x1）を、より大きな任意のサイズの正方形に詰め込むことだ。大きな正方形の辺の長さが整数でない場合、内部に配置／詰め込みできる1x1正方形の最大数を決定するのは自明でなくなる。
- DevelopingElk
個人的な変更を加えつつ、その証明の再現に取り組んでいる。基本的なアプローチは、標準的なコンピュータ支援による「不可避集合」手法だ。まず、2つの正方形の中心が同じ領域に収まらない程度に小さい領域をいくつか選ぶ。記事では16を使っていた。各領域は正方形を含むか含まないかのどちらかで、これは16 choose 11通り、約2000ケースになる。各ケースについて、それを除外しようと試みる。これは、正方形で覆われなければならない領域を特定し、その情報を伝播させることで行う。Stromquistが1989年に行ったようなパッキングLPを使って、さらに多くの構成を除外することもできる。その後、残ったケースに絞り込み、さらに細分化していく。
AI以前にこれが行われなかった唯一の理由は、真剣に注目されるトピックではなかったからだと思う。1989年のコンピュータは、すべてのケースを扱うには非力すぎた。しかし、基本的な材料はケプラー予想の証明にすべて揃っていた。AIがやったのは、正方形詰め込みが好きなだけのアマチュアがそのような証明を実行し、形式的に検証できるほどに、労力を下げたことだ。私自身もそうしたアマチュアの一人だと考えている。つまりこれは、AIが数学者の証明を盗んだり、超人的なことをした事例ではなく、民主化の事例だ。AIが数学に与える影響やAI企業の振る舞いについては懸念しているが、これは心配すべき事例ではない。この配置が最適であることを証明するための計算は、常に手作業で確認するには大きすぎるだろう。しかし、パッキングLPやコアの重なりの素敵な可視化をいくつか作成したいと思っている […]
- dkural
一見したほど恣意的でも醜くもない - ここの画像と説明を参照：https://x.com/davidmbudden/status/2107646435659481548
- yzydserd
参考までに、正方形の中に正方形を詰め込む問題の主要サイトは https://kingbird.myphotos.cc/packing/squares_in_squares.html にある。三角形のビューが最も面白い。そしてこのビューに関する20分の動画はこちら：https://youtu.be/uL5wuiy34rs
- WithinReason
多くの正方形詰め込みのリストと画像：