This article is a re-publication of Rei-AIOS Blueprint Pilot v0.1 for the dev.to community.
The canonical version with full reference list is in the permanent archives below:
- Zenodo (DOI, canonical): https://doi.org/10.5281/zenodo.22051191
- GitHub source (private): https://github.com/fc0web/rei-aios Author: Nobuki Fujimoto (@fc0web) · ORCID 0009-0004-6019-9258 · License CC-BY-4.0 ---
Scope: STEP 614 + 622 + 623 + 624 THE_THEOREM chain, 48 theorems, zero sorry.
Date: 2026-08-09 pilot draft.
Origin: chat-Claude 2026-08-09 dialogue turn 7 offered content.tex骨格作成; 藤本さん Option A で 実行判断 pending → 2026-08-10 pilot 起動。
Migration plan: memory/project_blueprint_migration_candidate_2026-08-09.md
What is this?
A minimal leanblueprint-compatible blueprint for the Rei Collatz
proof-chain. The blueprint records LaTeX prose statements of 48
formalized theorems, tags each with \lean{fqname} (Lean 4
declaration name) + \leanok (fully formalized marker) + \uses{...}
(dependency DAG edges).
The point is not to prove Collatz (see honest scope in
src/content.tex Chapter 1 + Chapter 12). The point is to
demonstrate the leanblueprint methodology on a real Rei subset,
so that subsequent migration decisions can be based on operational
experience rather than concept.
Files
blueprint/
├── README.md (this file)
└── src/
├── content.tex Main body (Chapter 1-12, 48 theorems + prose + \uses DAG)
├── print.tex PDF wrapper (loads amsthm etc, calls \input{content})
├── web.tex HTML wrapper (for leanblueprint serve)
└── macros/
└── common.tex \lean, \leanok, \uses, \notready fallback definitions
To run locally (future)
Prerequisites: Python 3.10+, TeX Live 2023+, node.js (for leanblueprint serve).
pip install leanblueprint
cd data/lean4-transfer/blueprint
leanblueprint pdf # generates blueprint.pdf
leanblueprint serve # local server at http://localhost:8080 with dependency graph
leanblueprint checkdecls # verifies each \lean{name} resolves to a real Lean decl (requires proper lakefile.lean)
Caveat: checkdecls requires the underlying Lean project to be
lake build-clean with the STEP 614-624 files imported. Currently
data/lean4-transfer/ is a flat directory of standalone experimental
scripts without a lakefile.lean --- so checkdecls will not work
until stage (iii) of the migration plan (wire the STEP files into
data/lean4-mathlib/CollatzRei/ or create a dedicated
data/lean4-transfer/lakefile.lean project).
The \lean{name} tags in content.tex use bare declaration names
(matching the top-level theorem name in each STEP file). If the
migration moves declarations under a namespace CollatzRei prefix,
the \lean tags will need to be updated to the fully-qualified names
(e.g. CollatzRei.THE_THEOREM).
Honest scope (see src/content.tex Chapter 1 for full version)
- Zero sorry: 48 theorems, no acknowledged gaps at Carneiro's layer (3) (证明检查).
-
native_decide caveat: 12 theorems (batch_10000 + b1-b11) use
native_decide, which expands the TCB to the entire Lean compiler. This is explicitly flagged in Chapter 10 ("Batch Verification and Base Cases") and cross-referencesfeedback_zero_sorry_floor_not_ceiling.md2026-08-09 refine. - Not a Collatz proof: the genuine mathematical gap (trailing 1-bits >= 4 wall for n%32 in {15, 31}) is documented verbatim in Chapter 12 ("Honest Assessment: The Genuine Mathematical Gap").
- 2026-07-28 kernel bug context: This pilot was authored days after Lean 4 issue #14576. The STEP 614-624 chain uses only bare inductive types and is not directly affected. See Chapter 1 Remark 1.4 for details.
What this pilot demonstrates (Chapter 12 Remark 12.1 verbatim)
- (i) leanblueprint methodology applied to a real Rei stack subset.
- (ii) A working
\usesDAG that would allow color-coded formalization progress tracking if imported into a proper Lake project. - (iii) Explicit 4-layer TCB annotation per 2026-08-09
feedback_zero_sorry_floor_not_ceiling.mdrefine.
What this pilot does NOT demonstrate
- (a) A Collatz proof (see Chapter 12 gap).
- (b) Novel mathematical content beyond STEP 614-624 (produced 2026-04 to 2026-05, see CLAUDE.md).
- (c)
leanblueprint checkdeclssuccess (see "To run locally" caveat).
Next steps (藤本さん judgment)
- Stage (i) DONE (2026-08-10 pilot): content.tex 骨格 generated.
- Stage (ii) DONE (2026-08-10 pilot): ~40
\usesedges captured. - Stage (iii) PARTIAL (2026-08-10 Option D): lakefile.toml + lean-toolchain + CollatzChain.lean scaffolding created at
data/lean4-transfer/, but architectural constraint discovered (see below). - Stage (iv) PENDING:
leanblueprint servedeploy topublic/tools/rei-collatz-blueprint/per 2026-08-06 藤本さん永久 protocol.
Stage (iii) Option D — Architectural constraint findings (2026-08-10)
Created:
-
data/lean4-transfer/lakefile.toml(mathlib v4.27.0 依存、 pilot scope) -
data/lean4-transfer/lean-toolchain(leanprover/lean4:v4.27.0) -
data/lean4-transfer/CollatzChain.lean(namespace-wrapped 6 declarations: cs, ci, reaches1, exhaustive, exhaustive_parity, exhaustive_odd — pattern demonstration) -
data/lean4-transfer/.gitignore(Lake artifacts) - leanblueprint (v0.0.20) + rich_click 依存 installed globally.
Architectural constraint discovered:
leanblueprint (v0.0.20, client.py:238) uses git.Repo(...).working_dir to locate the lakefile:
lakefile_lean_path = Path(repo.working_dir)/"lakefile.lean"
lakefile_toml_path = Path(repo.working_dir)/"lakefile.toml"
This means leanblueprint expects the lakefile at the git repository root, not in a subdirectory.
For Rei-AIOS (single git repo with Lean projects in data/lean4-transfer/ + data/lean4-mathlib/ subdirs),
neither existing lakefile is at git root, so leanblueprint commands fail with:
Error: Could not find lakefile.lean or lakefile.toml in C:\Users\user\rei-aios
Verified: setting GIT_WORK_TREE / GIT_DIR env vars does not override this (GitPython calls git rev-parse --show-toplevel).
Stage (iii) full completion options (藤本さん judgment 領域):
| Option | Approach | Pros | Cons |
|---|---|---|---|
| (a) Move lakefile to git root | Add lakefile.toml at C:\Users\user\rei-aios\ | Direct fix | Breaks existing convention (data/lean4-mathlib/ is the canonical Lean project); risks name collision |
| (b) Git submodule | Make data/lean4-transfer/ its own git repo, add as submodule |
Isolates Lean project | Invasive restructuring; complicates rei-aios repo management |
| (c) Upstream leanblueprint PR | Fork PatrickMassot/leanblueprint to accept --project-root CLI option |
Cleanest long-term | Requires upstream review + release cycle |
| (d) Document limitation | Accept that stage (iii) checkdecls is not directly usable in current repo layout |
Zero further work | Blueprint DAG can still be built with leanblueprint pdf / serve, but declaration existence checking must be manual |
| (e) Wire into data/lean4-mathlib/ | Add step614-624 modules under data/lean4-mathlib/CollatzRei/Chain/ namespace |
Reuses existing Lake project | Still hits constraint (mathlib dir is also subdirectory); requires (a) first |
Recommendation (Rei-side reading, 藤本さん judgment 領域): Option (c) or (d) depending on priority. Option (a) has the highest structural risk (existing convention breakage per CLAUDE.md).
2026-08-10 追加 (Option D 完全化): 藤本さん Option (d) 「制約 accept + 手動 checkdecls」 選択 (Option (c) upstream PR は feedback-external-community-outreach-premature tension で 別 STEP)。
Rei-side 手動 checkdecls script 実装: scripts/check-lean-decls.ts (198 行 TypeScript)。
Usage:
cd C:/Users/user/rei-aios
npx tsx data/lean4-transfer/blueprint/scripts/check-lean-decls.ts
# Exit 0 if all decls found, 1 if any missing (CI-friendly)
2026-08-10 実行結果:
- Total
\lean{...}tags parsed: 67 (fqnameplaceholder comment 除外後) - Found in Lean files: 67 (100%)
- Missing: 0
- Duplicates (expected): 53 (STEP 614/622/623/624 standalone scripts で cs/ci/reaches1 等 重複定義、 standalone script 性質による intentional)
- Overall status: PASS
Honest scope:
- grep-based lookup、 Lean 4 kernel formal verification ではない
- Type signature 一致は verify しない (name 存在のみ)
- Duplicates expected: STEP 622/623/624 standalone scripts で
cs/ci/reaches1等 重複定義 (script 性質) - Kernel-level verification が必要な場合: Option (c) leanblueprint upstream PR or Option (e)
data/lean4-mathlib/CollatzRei/統合 が別途必要
この実装で achieved:
- ✅ Blueprint content.tex
\lean{...}tag 全 (67/67) が Lean file に 実在 verify - ✅ Rei-side 独自 checkdecls (grep-based approximation) が Option (d) 選択の operational instance
- ✅ CI-friendly exit code (0/1) で 将来 pre-commit hook / cron 統合 可能
Stage (iii) status 更新:
- (a) content.tex format = DONE
- (b)
\usesDAG = DONE (~40 edges) - (c) leanblueprint CLI 統合 = PARTIAL (leanblueprint upstream 制約 + Rei-side 手動 checkdecls script 代替実装で PASS)
- Overall stage (iii) = OPERATIONAL (Blueprint pilot の 「命題忠実性 = 人間責任」 layer が Rei-side script で automatable)
What Option D pilot demonstrated
- ✅ leanblueprint (v0.0.20) available in Rei environment
- ✅ Lake project scaffolding pattern (lakefile.toml + lean-toolchain + namespace-wrapped module)
- ✅ CollatzChain.lean = 6 core declarations from STEP 622-624 wrapped in
namespace CollatzChain(pattern for full 48-theorem migration) - ⚠ Architectural constraint: leanblueprint's git-root assumption incompatible with Rei sub-directory Lean project layout
- 📝 5-option decision matrix for stage (iii) full completion (藤本さん judgment)
What Option D pilot does NOT demonstrate
- (a)
lake updateexecution (not run; would fetch mathlib v4.27.0 ~15-30 min, network + disk cost) - (b)
lake build CollatzChainexecution (blocked by (a)) - (c)
leanblueprint checkdeclsexecution (blocked by architectural constraint above) - (d) Full 48-theorem namespace migration (only 6 core declarations wrapped as demonstration)
Related memory
-
feedback_no_rush_publication.md2026-08-09 addition (external technical追認 by chat-Claude) -
feedback_zero_sorry_floor_not_ceiling.md2026-08-09 refine (4-layer TCB gauge) -
project_session_2026-08-09_chat_claude_math_universe_arc.md(7 turn dialogue archival) -
project_blueprint_migration_candidate_2026-08-09.md(3-stage migration plan) - CLAUDE.md STEP 614-624 (source proof-chain)
