数学原稿の件数と Lean の形式化状況を集計するときは、何を 1 件として数えるかを先に決めます。OpenAI の数学原稿リポジトリでは、結果系列、原稿、形式化の出典、Lean の定理宣言がそれぞれ異なる単位で管理されています。公開側の README は 372 結果系列と 719 原稿を報告しています[1]。原稿数と研究成果の検証状態を区別する考え方は、既稿でも扱われています[2]。本記事では、この区別を Python の検査処理にします。
対象の Git リビジョンを固定し、CONTENTS.md の件数と lean/formalization.yaml の登録件数を別々に取得します。さらに、参照先の版が異なる原稿を検出し、どこまで一致したかを出力します。
数学原稿の件数と形式化情報は同じ単位ではない
確認対象のデータには、次の 4 種類の件数があります。
| 対象 | 件数 | 1 件が表すもの |
|---|---|---|
| 結果系列 | 372 | 関連する数学的結果をまとめた系列 |
| 原稿 | 719 |
preprints/ にある個別の原稿 |
| 形式化の出典 | 173 |
formalization.yaml の sources にある項目 |
| 主要結果の定理宣言 | 200 | 同ファイルの status.main_results にある項目 |
結果系列には、主要な結果、補足議論、別証明など、複数の原稿が属する場合があります。同様に、形式化の出典と Lean の定理宣言も一対一で対応するとは限りません。集計結果には、件数とともにその単位を表示します。
Python 3.12 で公開データを取得する
Linux または macOS のシェル、Git、Python 3.12 を前提とします。Git の部分チェックアウトを利用し、検査に必要な 4 ファイルを取得します[3]。リポジトリは更新されるため、以下のコミットを固定します。
git clone --filter=blob:none --sparse --no-checkout https://github.com/openai/math.git
cd math
git sparse-checkout set --no-cone /README.md /CONTENTS.md /history.md /lean/formalization.yaml
git checkout --detach 1581d4cbdd69a0faf34b2089614fe2a814316a6a
git rev-parse HEAD
最後のコマンドで 1581d4cbdd69a0faf34b2089614fe2a814316a6a と表示されることを確認します。チェックアウトするのは公開リポジトリの固定リビジョンです。
次に Python の仮想環境を準備します。YAML の解析には PyYAML 6.0.3 の safe_load() を使います[4]。
python3.12 -m venv .venv
. .venv/bin/activate
python -m pip install 'PyYAML==6.0.3'
python --version
python -c 'import yaml; print(yaml.__version__)'
Python 3.12.x と 6.0.3 が表示されることを確認します。
CONTENTS.md から結果系列数と原稿数を数える
CONTENTS.md では、結果系列が **001. のような見出しで始まり、個別原稿は  [タイトル](preprints/...) という行に置かれています[5]。
この構造に対し、次の抽出規則を使います。
- 結果系列：行頭の
**に続く 3 桁の系列番号とピリオド - 原稿：行頭の
 に続き、リンク先がpreprints/で始まる項目 - 重複検査：系列番号と原稿リンク先をそれぞれ集合にして一意性を確認
今回の版では系列番号は 001 から 377 の範囲にあり、欠番もあります。最大番号を件数として利用せず、実際に抽出した見出しを数えます。
README の公表件数とも照合します。書式が変わって抽出数がずれた場合は、件数を確定する前にエラーにします。
formalization.yaml の登録情報を検査する
lean/formalization.yaml は、形式化対象の出典を sources に、主要結果の形式化に対応する Lean 宣言を status.main_results に記載しています[6]。
主要結果の項目には、declaration、file、comparator_config が含まれます。これらはそれぞれ定理宣言名、Lean ソースの相対パス、Comparator の設定ファイルを示すメタデータです。
この検査では、各項目に必要な文字列が存在し、宣言名が重複していないことを確認します。Lean の型検査や Comparator の実行は行わないため、結果はメタデータの構造検査として記録します。
公開件数と形式化情報を照合する
リポジトリのルートに math_catalogue_check.py を次の内容で保存します。
from pathlib import Path
import re
import yaml
FAMILY_PATTERN = re.compile(r"^\*\*(\d{3})\.", re.MULTILINE)
PAPER_PATTERN = re.compile(
r"^[ \t]* \[[^\n]+\]\((preprints/[^)\n]+)\)", re.MULTILINE
)
README_PATTERN = re.compile(
r"current catalogue contains (\d+) manuscripts organized into (\d+) families"
)
HISTORY_PATTERN = re.compile(r"(\d+)\s*/\s*(\d+)\s*=\s*~(\d+)%")
def check_unique(name, values):
if len(values) != len(set(values)):
raise ValueError(f"duplicate {name}")
def main():
root = Path(__file__).resolve().parent
readme = (root / "README.md").read_text(encoding="utf-8")
contents = (root / "CONTENTS.md").read_text(encoding="utf-8")
history = (root / "history.md").read_text(encoding="utf-8")
with (root / "lean/formalization.yaml").open(encoding="utf-8") as f:
catalogue = yaml.safe_load(f)
families = FAMILY_PATTERN.findall(contents)
papers = PAPER_PATTERN.findall(contents)
check_unique("family numbers", families)
check_unique("manuscript paths", papers)
published = README_PATTERN.search(readme)
if published is None:
raise ValueError("README catalogue counts not found")
claimed_papers, claimed_families = map(int, published.groups())
if (len(papers), len(families)) != (claimed_papers, claimed_families):
raise ValueError("README and CONTENTS.md counts disagree")
sources = catalogue["sources"]
results = catalogue["status"]["main_results"]
source_paths = []
for source in sources:
path = source["id"]
if not isinstance(path, str) or not path.startswith("../preprints/"):
raise ValueError(f"unexpected source path: {path}")
source_paths.append(path.removeprefix("../"))
check_unique("source paths", source_paths)
declarations = []
for result in results:
for key in ("declaration", "file", "comparator_config"):
if not isinstance(result.get(key), str) or not result[key]:
raise ValueError(f"missing or invalid main-result field: {key}")
declarations.append(result["declaration"])
check_unique("Lean declarations", declarations)
report = HISTORY_PATTERN.search(history)
if report is None:
raise ValueError("history formalization ratio not found")
reported_formalized, reported_total, reported_percent = map(int, report.groups())
if reported_total != len(papers):
raise ValueError("history denominator and manuscript count disagree")
unmatched = sorted(set(source_paths) - set(papers))
print(f"result_families: {len(families)}")
print(f"manuscripts: {len(papers)}")
print(f"formalization_sources: {len(sources)}")
print(f"main_result_declarations: {len(results)}")
print(f"unmatched_source_paths: {len(unmatched)}")
for path in unmatched:
print(f" {path}")
print(
"reported_formalized_top_line_results: "
f"{reported_formalized}/{reported_total} (~{reported_percent}%)"
)
print(f"yaml_scope: {catalogue['status']['scope']}")
print(f"yaml_review: {catalogue['review']['status']}")
if __name__ == "__main__":
main()
実行します。
python math_catalogue_check.py
対象コミットのファイルを解析すると、次の件数になります。
result_families: 372
manuscripts: 719
formalization_sources: 173
main_result_declarations: 200
unmatched_source_paths: 1
preprints/Taming-implies-compatibility-on-four-manifolds-September-23-2026/paper.pdf
reported_formalized_top_line_results: 300/719 (~42%)
yaml_scope: Partial progress.
yaml_review: unchecked
これらの件数と不一致パスは、固定コミットの公開ファイルの内容を確認した値です。Python スクリプト自体は同じ形式の模擬データで正常系と異常系を実行しており、公開リポジトリをローカルでチェックアウトして実行した結果とは区別しています。
unmatched_source_paths は、形式化カタログが示す出典パスのうち、現在の CONTENTS.md の原稿リンクに同じ文字列が見つからなかった件数です。今回の 1 件については、現在の原稿一覧に次のパスが掲載されています。
preprints/Taming-implies-compatibility-on-four-manifolds-October-6-2026/paper.pdf
両者はディレクトリー名に含まれる日付部分が異なります。これはカタログの参照と原稿一覧との版の相違を確認する手掛かりです。ファイル名の日付を公開日とみなしたり、参照先の相違だけで証明の正誤を判定したりする処理は行いません。
history.md の撤回・修正履歴と件数を区別する
history.md は、3 原稿の撤回、14 原稿の修正、形式化情報の追加を記録しています。また、主要結果の形式化状況として 300 / 719 = ~42% と記載しています[7]。
検査スクリプトは、履歴上の分母 719 と現在の原稿件数が一致することを確認します。一方、分子 300 は公開側の報告値として出力し、YAML の sources 173 件や main_results 200 件から再計算しません。
history.md は変更履歴です。撤回された原稿の理由や改訂の存在を調べる資料として使い、各原稿の最新検証状態を一覧化したデータとは区別します。
件数集計から判断できる検証範囲
今回のスクリプトで確認できるのは、固定リビジョンにおけるカタログの件数、構造、相互参照の一致状況です。終了状態の判断には、次の区別を使います。
| 検査結果 | 確認できること | 別途必要な検証 |
|---|---|---|
| 件数の一致 |
README.md と CONTENTS.md の数量が一致 |
個々の数学的主張の正しさ |
| YAML の解析成功 | 形式化メタデータの項目を読み取れた | Lean による定理宣言の受理 |
| 宣言名の一意性 | 同一名の重複登録がない | 公理依存や証明対象の妥当性 |
| 出典リンクの一致 | 2 つのカタログが同じ相対パスを参照 | 原稿本文と形式命題の対応 |
| 履歴の分母一致 | 公表された原稿総数との整合 | 公表された形式化率の独立再計算 |
YAML には status.scope: Partial progress. と review.status: unchecked が記載されています。登録情報を取得できたことを、形式的検証や査読の完了へ拡張して解釈する根拠にはなりません。Lean の型検査と公理依存を実際に確認する手順は、別記事で扱っています[8]。
まとめ
固定コミットで集計すると、372 結果系列、719 原稿、173 出典、200 定理宣言が得られます。また、形式化の出典パスと原稿一覧の間に、版の違いによる不一致が 1 件見つかります。
原稿の公開規模を示す値、形式化カタログの登録内容、公開側が報告する形式化率は、それぞれ独立した指標として保持します。300 / 719 は履歴に記載された報告値であり、200 / 719 を同じ形式化率の代替値として扱う根拠はありません。集計対象と検証の範囲を明記することで、更新された原稿一覧についても同じ手順で差分を確認できます。
参考文献
- OpenAI, Readme. https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/README.md
- id774, 証明はいつ数学的知識になるのか（2026-10-09）. https://blog.id774.net/entry/2026/10/09/5760/
- Git Project, git-sparse-checkout Documentation. https://git-scm.com/docs/git-sparse-checkout
- Kirill Simonov, PyYAML（2025-09-25）. https://pypi.org/project/PyYAML/6.0.3/
- OpenAI, Mathematics manuscript collection. https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/CONTENTS.md
- OpenAI, OpenAI math repository. https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/lean/formalization.yaml
- OpenAI, History. https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/history.md
- id774, AI 生成証明を Lean 4 の型検査と公理監査で検証する（2026-09-08）. https://qiita.com/ynakayama/items/82d955c49be465d623f8