Lean

openai/math

OpenAI内製モデルが生成した数学研究論文集 — OpenAIの内部モデルが未解決の数学研究問題に挑んだ成果を集めたリポジトリです。722本の数学的原稿を372のファミリーに分類し、一部はLeanによる形式証明付きで公開されています。AIが数学研究にどこまで迫れるかを示す貴重な実例資料です。

stormj-UH/spivak-lean

Spivak微積分学を丸ごとLean 4で形式化 — Michael Spivakの名著『Calculus』第3版・第4版の全30章と付録9本の定義・定理・問題をLean 4で形式化したプロジェクトです。Spivak自身の独自定義（ε-δ論法や上下和積分など）を基点にMathlibの関数と同一視し、さらにeやπの超越性証明、Liouvilleの定理まで踏み込んでいる点が特徴で、形式化数学や解析学に関心のある人に刺さる内容です。

Michael Spivak's Calculus formalized in Lean 4: every theorem and every problem of all 30 chapters and 9 appendices, in both the 3rd and 4th editions

Queuingtheorydotcom/11SquaresFormalized

11個の正方形パッキング最適性のLean証明 — 単位正方形11個を最小の正方形に詰める問題の最適性証明をLeanで形式化したリポジトリです。7,920個のLeanモジュールを検証し、admit（未証明箇所）ゼロを達成しています。数値証明の一部はnative_decideを用い、Leanカーネルとネイティブコンパイラを信頼する形で最適辺長の厳密な証明を完成させています。

Lean formalization of the optimality proof of the 11 square packing