Tau Ceti：AIがコードを書く形式数学ライブラリ、Mathlibと補完関係

Tau Ceti は、AI がコードを書き、人間がロードマップを提供する形式数学ライブラリです。Lean FRO と Mathlib Initiative がインキュベートし、学術界および産業界と連携しています。このプロジェクトの核心は、人間の数学者がロードマップを策定し、AI システムがそれに従ってコードを実装する点にあります。すべてのコントリビューションは AI 駆動のレビュープロセスを経ており、レビュールールは人間が作成し TauCetiReview リポジトリで公開されています。Tau Ceti は Mathlib と補完関係にあり、Mathlib の上に構築されつつも、精緻なキュレーションよりも迅速な再利用可能なライブラリの構築に重点を置いています。プロジェクトの目標は、大規模な形式化を通じて数学の研究フロンティアに貢献することです。

レビュープロセスは敵対的であり、誤った形式化や空疎な文を見つけることを目的としています。AI は固定のオープンソースルーブリックに従って動作し、PR が開かれるとまず CI が実行され（Mathlib のリンターセットを含む）、その後ルーブリックに基づいて「ブロック」「変更要求」「承認」の判定が下されます。現在、レビューインフラは構築されていますが自動化はされておらず、コマンドラインから実行できます。さらに、「メタレビュー」システムもプロトタイプとして開発されており、人間と AI の審査員がレビューの A/B テストを行い、レビューの品質を定量的に評価します。

Tau Ceti は Mathlib の master ブランチに依存し、Mathlib の設計決定に常に従います。AI は Mathlib の新しいコミットにピンを更新し、それに伴う問題を修正する PR を提出することが推奨されています。プロジェクトから Mathlib へのアップストリームは行われませんが、Mathlib のコントリビューターは Tau Ceti の素材を自由に採用、整理、変更できます。すべてのコードは Apache ライセンスの下で公開されています。

このプロジェクトは、Mathlib のような人間によるキュレーションを目指すものではなく、スケーラブルで再利用可能なオープンライブラリの構築に焦点を当てています。Tau Ceti の哲学は、数学の成果は明確さと理解であり、定理そのものではないというものです（ビル・サーストンの言葉を引用）。AI が書いた定義に対する信頼は、最初のレビューではなく、それらをより深い数学のネットワークに統合し、その上でさらに定理を証明することで構築されると期待されています。

コラボレーションに関しては、Tau Ceti は「意図登録」メカニズムを採用しており、コントリビューターが現在作業中のロードマップ項目を宣言することで重複を防ぎます。このメカニズムは内部で既に使用されており、将来的には公開プロジェクト意図登録簿に拡張され、連邦システムへと発展する可能性があります。プロジェクトは迅速な開発を重視し、フロンティア研究の妨げにならないように配慮しています。Tau Ceti はコミュニティリソースであり、すべての人の参加を歓迎します。