Lean 4ソフトウェアスケーリング則
本稿では、Lean 4のコードベースにおいて、ソフトウェアのスケーリング則（scaling laws）を検証する。具体的には、プロジェクトの規模や依存関係の増加に伴い、コンパイル時間やメモリ使用量、証明の複雑さがどのように変化するかを分析し、大規模な形式検証プロジェクトにおける効率的な開発手法について考察する。
背景メモ
- リーン数学（Lean）は、Microsoft Researchが主導する定理証明支援系（対話型証明アシスタント）で、数学者がコンピュータで検証可能な形で証明を記述できるようにするもの。Lean 4は2021年にリリースされた最新メジャーバージョン。
- 「スケーリング則」は、もともと機械学習（大規模言語モデル）の分野で、モデルサイズやデータ量を増やすと性能が予測可能に向上する現象を指す概念。GwernはこれをLeanでの定理証明タスクに応用し、より多くの証明を書くことでシステム全体の証明能力が向上するかを検証している。
- Gwern.netは、Gwern Branwen（独立研究者）が運営する個人サイト。AI、統計、薬理学など多岐にわたるテーマを扱い、長文の深堀りエッセイで知られる。特にAI安全性とスケーリング則に関する考察で注目を集めている。
- この記事の背景にある問題意識：形式的検証（formal verification）はソフトウェアのバグを潰す強力な手法だが、証明を書くコストが高く普及の障害になっている。もし「証明を大量に書くだけで自動的に証明能力が向上する」スケーリング則が成立すれば、Leanの実用化が一気に進む可能性がある。