facebookresearch/atlas-lean

ATLAS – 大規模自動形式化教科書ライブラリ

概要 – ATLAS は、Lean 4 証明支援系で形式化された研究グレードの数学ライブラリです。コードベースには、コア数学ライブラリ（Mathlib）を拡張し、学部および大学院の教科書から抽出された新しい定理と定義を追加するいくつかの Lean パッケージが含まれています。形式化作業は、大規模言語モデルを使用して教科書の記述と証明を Lean コードに変換する自動形式化パイプライン（AutoformBot）によって駆動されます。

重要性 – 形式化された数学により、人間と機械の両方が数学的結果を絶対的な確実性で推論できます。教科書の内容を自動的に再利用可能な Lean ライブラリに変換することで、ATLAS は以下に使用できる大規模で高品質な形式化ライブラリの作成を加速することを目指しています：

• 解析学、代数学、幾何学、位相幾何学、確率論、統計学、理論計算機科学における検証済み研究。
• 定理証明を支援する AI システムのトレーニングと評価。
• プロジェクト間で参照できる機械検証可能な数学の共有リポジトリの構築。

主要コンポーネント

コンポーネント	役割
MathlibExt/	標準 Mathlib ライブラリへの新しく完全に証明された拡張。
MathlibExtTest/	MathlibExt の拡張に対するテスト、ベンチマーク、診断。
CSLibExt/	MathlibExt 上に構築された形式化された計算機科学の結果。
CSLibExtTest/	計算機科学拡張のテストと診断。
WantedExt/	特定されたがまだ形式化されていない重要な結果のプレースホルダー。

リポジトリには、ルート Lake パッケージの完全な検証スイートを実行する check.sh スクリプトを含む scripts/ フォルダも含まれています。

開始方法

1. Lean 4（v4.34.1 以降）と Lake ビルドツールをインストールします。
2. リポジトリをクローンし、ルートチェックを実行します：

   scripts/check.sh
   

3. Lean 互換エディタ（例：Lean 拡張機能付きの VS Code）で .lean ファイルを開いてライブラリを探索します。
4. 元のより大きな形式化教科書コレクションについては、アーカイブされた v1/ ディレクトリに切り替えてビルドします：

   cd v1
   lake build
   

   v1 リリースには、評価レポート、ドキュメント、および関連研究論文も含まれています。

ステータス – 現在のリポジトリには、活発に開発中の ATLAS v2 の足場が含まれています。以前の v1 リリースはアーカイブされていますが、完全に機能し、文書化されています。

ライセンス – 新しい貢献は Apache 2.0 ライセンスの下にあります。アーカイブされた v1/ コードは元のライセンスのままです。

---

ATLAS は、形式手法と AI 駆動の自動化の交差点にある本物の研究プロジェクトであり、チュートリアルリストや簡単なデモではありません。