---
name: project-step1357-palomar-registry-paper130-141-mapping-2026-08-21
description: "STEP 1357 Palomar Registry × Paper 130/141 mapping arc. Terry Tao 2026-08-18 blog post 発見 (Research Radar 2026-08-20) → 藤本さん (a) 承認 → Palomar operational 要点 fetch + Paper 130 (Open Problems META-DB) + Paper 141 (Power×Thermo×D-FUMT₈) との mapping 分析 + site page 反映. Option A-E defer, 実 submit は 別 STEP."
metadata: 
  node_type: memory
  type: project
  originSessionId: 995adcb1-1892-4d63-83ac-ddbae2b50247
  modified: 2026-08-20T15:48:42.045Z
---

# STEP 1357 — Palomar Registry × Paper 130/141 mapping

**Date**: 2026-08-21
**Type**: discovery + mapping analysis + site 反映 (実 submit なし = defer)
**Origin**: Research Radar 2026-08-20 で Terry Tao 2026-08-18 blog post "Palomar — a registry of Lean verified mathematics" 発見 → 藤本さん judgment (a) 承認

## Why

Rei stack は 現在 Zenodo + GitHub + note.com + 11 platform (Paper 130-142) で 論文発表チャネル確保済、 但し **Lean 4 formal proof を external verification で 直接 verify する registry 経路** は未確立。 Palomar は Lean 用 arXiv 相当の preprint server、 mechanical Comparator + LLM semantic match の minimal check で **individual Lean theorem を external verified stamp 付き 参照可能に する** = Rei stack Paper 141 (15 theorem / 0 sorry / 1 axiom) + STEP 614-624 Collatz 645+ axiom-free theorem の external channel candidate。

## How to apply

- **Palomar は preprint server = journal ではない** (Tao 本文中 strong 否定)。 submit しても publication credit なし、 Zenodo DOI 代替にはならない。 「novelty check なし = minimal」 の scope 厳守。
- **Paper 141 が pilot 最適** (単一 file / 15 theorem / 0 sorry / 1 axiom disclosure / Zenodo DOI 既取得 = 4 条件揃う)。 Paper 130 は index layer で 直接 submit 対象でない (7-type × D-FUMT₈ meta-classification は Palomar 対応 field なし)。
- **early-adopter risk 認識**: 2026-08 時点 verified entry 1 件 (Sendov) のみ = spec 変更 / registry 停止 の 可能性、 Rei stack 全 theorem を 一括化する現時点計画なし。 pilot 1-3 件で stance judgment。
- **世界唯一主張 impose しない** ([[feedback-world-uniqueness-claim-controllable]])。 「Palomar に D-FUMT₈ tag を要望」 は現段階 scope 外、 Rei stack 独自 metadata は formalization.yaml `extra:` field or 別 Rei 側 index に格納。

## Palomar operational 要点

- URL: **palomar-registry.org**
- 母体: **Lean FRO** + **ICARM** 共同 initiative
- SAB: **Terry Tao** + Avigad + Ballard + de Dios + Guillen + Bryna Kra + Kim Morrison + Ravi Vakil + Akshay Venkatesh
- 位置付け: "zeroth approximation of a preprint server for Lean proofs" (Tao 自身)
- 受け入れ: 外部 GitHub specific commit snapshot (registry 自身は host しない、 mirror でなく参照登録)
- 3 file 必須:
  1. **challenge file** — Lean 主張、 hard cap **1000 行 / 100 KB**、 推奨 300 行前後
  2. **solution module** — 任意長 proof
  3. **formalization.yaml** — informal description + metadata + disclosure (schema `github.com/mathlib-initiative/formalization.yaml`)
- 依存 escape hatch: **Tau Ceti repository** (taucetiproject.github.io/TauCeti)
- verify 2 段:
  - (a) **mechanical**: Lean Comparator (github.com/leanprover/comparator) で type-check + 主張一致
  - (b) **non-deterministic**: LLM が informal description ↔ Lean 主張 意味的一致 check
- governance: **人手 peer review なし**、 arXiv 型 scale 想定、 第三者 review layer 積上げ 歓迎
- 実 test 済 entry: **PALOMAR-2026-08-13-000001** (Tao Sendov's conjecture、 github.com/teorth/sendov)
- discussion: Zulip `leanprover.zulipchat.com/#narrow/channel/621638-Palomar`

## Paper 130 mapping (index layer)

Paper 130 (Open Problems META-DB、 DOI [10.5281/zenodo.19700758](https://doi.org/10.5281/zenodo.19700758)、 2026-04-23、 713 problems v2 = 2,583 entry)。 public repo = github.com/fc0web/rei-open-problems、 dataset DOI zenodo.19709764。

**Mapping 結論**: Paper 130 自体は **submit 対象でない** (meta-classification layer、 Palomar は 個別 challenge/solution registry)。 Paper 130 の 役割は **Palomar entry への 上位索引** = 「どの Rei theorem が どの open problem に対応するか」。 formalization.yaml disclosure ↔ Rei `sorryCount + lean4: scaffold` field 直接互換化可能。

## Paper 141 mapping (pilot 最適)

Paper 141 (Power × Thermodynamics × D-FUMT₈、 DOI [10.5281/zenodo.19832874](https://doi.org/10.5281/zenodo.19832874)、 2026-04-27 STEP 1002)。 15 theorem / 0 sorry / 1 axiom (Bennett reversibility placeholder) / 単一 file `data/lean4-mathlib/CollatzRei/PowerThermodynamics.lean` / Lean 4 v4.27.0 + Mathlib pinned。

**Mapping 結論**: Palomar test submit pilot として **4 条件揃う**: challenge file 300 行前後 (推奨内)、 axiom formalization.yaml disclosure 記載可、 sorry 0 = Comparator pass 前提、 Zenodo DOI 既取得。 Bennett axiom は "explicit axiom" として 登録、 Palomar Comparator が axiom-based を "proof" と扱うかは Sendov 先行 case 確認要 (novelty judgment なし = 通る可能性大)。

## Option A-E (藤本さん judgment 待ち)

- **A** — Paper 141 test submit pilot (工数 4-6 時間、 blast radius 中)
- **B** — Paper 130 META-DB schema Palomar-compat field 追加 (工数 2-3 時間、 blast radius 小)
- **C** — STEP 623 v3 Collatz Cases 1-4 (8 定理) 1 entry pilot (工数 3-5 時間、 blast radius 中)
- **D** — Zulip 参加 + Palomar spec 深掘り (工数 1-2 時間 aleatory、 blast radius 極小)
- **E** — 発見報告 + site 反映のみ close、 defer (工数 現状のみ、 blast radius ゼロ)

私 prefer 順: **D → E → B → A → C**

## Honest scope 7 条

(i) preprint server = peer-reviewed journal ではない、 publication credit 発生せず / (ii) minimal check のみ = novelty/interest/accuracy 判定なし / (iii) Tau Ceti spec は 未取得 = 大 dependency import 時 別途 fetch 要 / (iv) 2026-08 時点 verified entry 1 件 (Sendov) のみ = early-adopter risk (spec 変更 / registry 停止 の 可能性) / (v) Rei stack 645+ theorem 全体 Palomar 化計画なし = pilot 1-3 件で stance judgment / (vi) Paper 130 の 7-type × D-FUMT₈ は Palomar 対応 field なし = 世界唯一主張 impose せず / (vii) autoformalization 議論は Rei-PL Prover v0.1 (Paper 137、 DOI zenodo.19821866) mapping と 別軸 = 別 STEP candidate。

## site page

- **URL**: https://rei-aios.pages.dev/tools/step-1357-palomar-registry-mapping/
- **file**: `public/tools/step-1357-palomar-registry-mapping/index.html` (~15 KB self-contained HTML、 7 section)
- **mirror**: `dist-renderer/tools/step-1357-palomar-registry-mapping/index.html` force-track md5 一致 `3c98c74531e66f461a5adc75ed41990f`
- **verify**: CF Pages deploy 1-3 分後 HTTP 200 予定

## 関連

- [[project-step1354-d8-neither-landing-page-2026-08-20]] (別タブ、 教材 arc)
- [[project-step1353-statistics-neither-education-v01-2026-08-20]] (別タブ、 教材 arc)
- [[project-step1352-memory-mirror-arc-2026-08-20]] (別タブ、 memory mirror)
- [[feedback-no-rush-publication]] (「急がずゆっくりと」 = 単日 close、 実 submit は判断後 別 STEP)
- [[feedback-world-uniqueness-claim-controllable]] (世界唯一主張ゼロ discipline 継承)
- [[feedback-zero-sorry-floor-not-ceiling]] (0 sorry = floor discipline、 Palomar Comparator pass 前提条件と整合)
- [[feedback-one-reproduction-over-ten-unverified]] (「一の再現 > 十の未検証」 順序原則、 Option A の pilot 1 件 vs 全体化 の判断基準)
- [[feedback-all-research-site-reflection-default]] (2026-08-06 全研究 site 反映 default protocol)
- [[feedback-chat-claude-hallucination-warning]] Pattern 5-B (「近隣物との誤 conflate」 = Palomar ≠ Paper platform、 registry ≠ journal 区別厳守)

## Paper 130 index reference

- Paper 130 main: `papers/paper-130-open-problems-meta-db.md` (398 行、 7-type × D-FUMT₈ meta-classification)
- Paper 130 addendum v2: `papers/paper-130-addendum-v2-public-release.md` (185 行、 v1→v2 multi-tier schema、 public release)
- Paper 141: `papers/paper-141-power-thermodynamics-dfumt8.md` (210 行、 15 theorem / 0 sorry / 1 axiom detail)

## commit

- (本 STEP commit hash は commit 実行後に確定)