2026-08-20 の Research Radar 実行で、 Terry Tao 2026-08-18 blog post "Palomar — a registry of Lean verified mathematics" が Tao blog fetcher の 1 relevant post として上がった。 Palomar は Lean FRO + ICARM 共同 initiative、 Lean 用 arXiv 相当の 予稿サーバ (Tao 自身の表現で "zeroth approximation of a preprint server for Lean proofs")。 URL: palomar-registry.org。 Scientific Advisory Board = Tao + Avigad + Ballard + de Dios + Guillen + Bryna Kra + Kim Morrison + Ravi Vakil + Akshay Venkatesh。
藤本さんに 発見報告後、 (a) 「Palomar registry の 詳細 fetch + Paper 130/141 との mapping」 承認で 本 STEP 起動。
github.com/mathlib-initiative/formalization.yaml)依存 definitions が Mathlib 未収録 & 巨大な場合の逃げ道 = Tau Ceti repository (taucetiproject.github.io/TauCeti) を dependency として import。
Comparator (github.com/leanprover/comparator) で solution が (i) type-check し (ii) challenge file の主張を そのまま証明していることを 機械確認両者 pass で登録可。 Tao 明示: これは novelty / interest / accuracy 判定でなく、 「minimal check」 のみ。
PALOMAR-2026-08-13-000001 (Tao の Sendov's conjecture、 github.com/teorth/sendov)leanprover.zulipchat.com/#narrow/channel/621638-PalomarPaper 130: DOI 10.5281/zenodo.19700758 (2026-04-23)、 713 open problems (v2 では 2,583 entry) を 7-type × D-FUMT₈ 8 値で分類、 各 entry に formalization.sorryCount + formalization.lean4: "scaffold" field。 公開 repo = github.com/fc0web/rei-open-problems、 dataset DOI zenodo.19709764。
| Palomar formalization.yaml | Rei Paper 130 schema | 互換性 |
|---|---|---|
| project.name | problem id (例 erdos-1) | ✅ 直接 mapping |
| project.description (informal 記述) | statement.en / statement.latex | ✅ 直接 mapping |
| disclosure (axiom/sorry 開示) | formalization.sorryCount + formalization.lean4 | ✅ ★ Rei 側 field 完全既存 |
| challenge file (Lean 主張) | reiTyping.primaryType + dfumt8 | ⚠ 直接 mapping なし (Rei 側は meta-classification、 Palomar は 具体的 Lean 定理主張) |
| solution module | Lean 4 formalization file (data/lean4-mathlib/CollatzRei/*.lean) | ⚠ Rei 側 個別 problem に対応する Lean 4 file は 一部のみ (STEP 614-624 等) |
Mapping 結論: Paper 130 は meta-classification layer、 Palomar は 個別 challenge/solution registry。 直接 submit する対象は Paper 130 自体でなく、 Paper 130 が 索引する 個別 Rei Lean 4 file。 Paper 130 の役割は Palomar entry への 「どの Rei theorem が どの open problem に対応するか」 の 上位索引。
Paper 141: DOI 10.5281/zenodo.19832874 (2026-04-27、 STEP 1002)、 15 theorem / 0 sorry / 1 axiom (Bennett reversibility placeholder)。 単一 Lean 4 file = data/lean4-mathlib/CollatzRei/PowerThermodynamics.lean。
| 項目 | Paper 141 実測 | Palomar 適合 |
|---|---|---|
| challenge file 規模 | 15 theorem statement | ✅ 300 行前後 = 推奨範囲内、 1000 行 cap 余裕 |
| solution module 規模 | PowerThermodynamics.lean 全体 | ✅ 任意長 (Palomar は solution 長 制限なし) |
| Lean 4 版数 | v4.27.0 + Mathlib rev pinned | ✅ Palomar 前提 (Lean 4) |
| axiom disclosure | 1 axiom (bennett_reversibility) | ✅ formalization.yaml disclosure に explicit 記載可 |
| sorry count | 0 | ✅ Palomar Comparator pass 前提条件 |
| informal description | Abstract + Part A/B (Paper 141 本文) | ✅ formalization.yaml の project.description に 直接流用可 |
Mapping 結論: Paper 141 は Palomar test submit pilot として最適。 単一 file / 単一 axiom / 0 sorry / Zenodo DOI 既取得 = 4 条件揃う。 但し: Bennett axiom を disclosure でなく "explicit axiom" として 登録する場合、 Palomar Comparator は axiom を 使う theorem を "proof" と扱う可能性があり、 Tao の Sendov entry 等の 先行 case を 確認する必要 (novelty judgment なし = axiom-based も 通る可能性大)。
Paper 141 (15 theorem / 0 sorry / 1 axiom / 1 file) を Palomar test submit。 3 file 準備 + formalization.yaml 起草 + Comparator local run + submit。 想定工数: 4-6 時間 (formalization.yaml schema 学習 + submit プロセス initial trial 込)。 blast radius = 中 (Rei stack 側は既存 Paper 141 file 無変更、 Palomar 側で登録試行のみ、 拒否時は撤回可能)。
各 problem entry に palomar_ref: {entry_id: "PALOMAR-YYYY-MM-DD-NNNNNN", submitted: bool, verified: bool} field 追加。 v2 → v3 schema evolution として addendum 起草。 Palomar entry 化した Rei Lean 4 file を 明示 index 化。 想定工数: 2-3 時間 (schema 拡張 + INDEX.json 再生成 + addendum v3 markdown)。 blast radius = 小 (Paper 130 は Rei 側 内部改訂、 現行公開 DOI zenodo.19700758 は不変)。
Rei stack 645+ axiom-free Collatz theorem のうち、 step623_v3.lean (8 定理、 Cases 1-4 ∀n explicit descent) を 1 Palomar entry として test submit。 challenge file cap 適合確認 + Comparator pass 確認 + Rei stack Collatz の external verification 第 1 step。 想定工数: 3-5 時間。 blast radius = 中。
leanprover.zulipchat.com/#narrow/channel/621638-Palomar に 参加して 実 submission workflow / 拒否条件 / axiom-based entry 扱い を 聴取。 Rei stack 側は本 STEP の site 反映 + memory 記録のみで close、 実 submit は community 実態把握後の 別 STEP。 想定工数: 1-2 時間 (aleatory)。 blast radius = 極小。
本 STEP の site 反映 + memory 記録で終了、 実 submit / schema 拡張は defer。 「急がずゆっくりと」 feedback_no_rush_publication 継承、 藤本さん stance shift 待ち。 想定工数: 現状の close 作業のみ。 blast radius = ゼロ。
extra: field (schema で許容される場合) に格納するか、 別途 Rei 側で index 保持。 「Palomar に D-FUMT₈ tag を要望」 は現段階で scope 外 ([[feedback-world-uniqueness-claim-controllable]] 適用、 世界唯一主張 impose せず)。本 STEP は discovery + mapping 分析 + site 反映 で close。 Option A-E から 藤本さん判断待ち、 選択次第で 別 STEP 起動。 Auto Mode 下で 私が prefer する順は D → E → B → A → C (community 実態把握 → close → schema 拡張 → pilot submit → Collatz entry) だが、 藤本さん stance 次第で 順序は変更可能。