DEV Community

Nobuki Fujimoto
Nobuki Fujimoto

Posted on

Rei-PL Prover v0.1: A D-FUMT-8-Native Proof Assistant Prototype (Paper 137)

#lean #math #research #ai

This article is a re-publication of Rei-AIOS Paper 137 for the dev.to community.
The canonical version with full reference list is in the permanent archives below:

Author: Nobuki Fujimoto (藤本 伸樹) with Rei-AIOS (Claude Opus 4.7)
Contact: note.com/nifty_godwit2635 · Facebook: Nobuki Fujimoto · fc2webb@gmail.com
Date: 2026-04-24
License: Code AGPL-3.0 / Data CC-BY 4.0
Template: 4+7 要素構造 v2 (Parts A–K)
Companion papers: Paper 130 (Open Problems META-DB), Paper 133 (Sylvester-Schur), Paper 134 (AI tooling), Paper 135 (self-reference cluster)

Abstract

This paper introduces Rei-PL Prover v0.1, a prototype D-FUMT₈-native proof assistant that complements Lean 4 / Mathlib by providing native eight-valued propositional semantics. Unlike Lean 4's two-valued Prop, Rei-PL Prover's base judgment carries one of 8 truth values (TRUE / FALSE / BOTH / NEITHER / INFINITY / ZERO / FLOWING / SELF), enabling direct machine verification of D-FUMT₈ laws that Lean 4 can only encode via opaque axioms.

Verified (this paper)

  • 160-line prototype implementation in src/rei-pl-prover/ (4 modules: types, checker, theorems, lean4-export).
  • 3 toy theorems machine-checked:
    • Peace Axiom #196 = TRUE (foundational invariant)
    • AND(BOTH, BOTH) = BOTH (Belnap 4-valued idempotence)
    • AND(FLOWING, FLOWING) = FLOWING (Heraclitus impermanence composition)
  • 16/16 unit tests pass (test/step997-rei-pl-prover-test.ts).
  • One-way Lean 4 export bridge: each Rei-PL judgment exports as a Lean 4 theorem that compiles cleanly under Mathlib v4.27 (data/lean4-mathlib/CollatzRei/Step997ReiPLExport.lean, lake env lean → exit 0).
  • Peace Axiom #196 invariant enforced by the checker: any judgment whose claimed value mismatches the proof-term's computed value is rejected (CLAIM-VALUE MISMATCH error).

Honest positioning

  • This is a prototype, not a production proof assistant. 160 LOC total; compare to Lean 4 core ≈ 50,000 LOC.
  • The Lean 4 export is lossy: D-FUMT₈ non-classical values become opaque Prop axioms with inhabitation axioms; Lean 4 verifies proof-term shape but not D-FUMT₈ semantics.
  • No Mathlib-equivalent library in D-FUMT₈ idiom yet — that is the Phase 2 Paper 138+ direction.
  • No self-hosting yet — Phase 3 Paper 139+.
  • No neural tactic search integration — Phase 4 Paper 140+.

What this paper does claim

  1. D-FUMT₈ proof assistant is implementable (existence demonstrated).
  2. Three toy theorems genuinely require 8-valued semantics — they cannot be directly expressed in Lean 4 Prop.
  3. The Lean 4 bridge establishes co-evolution feasibility — Rei-PL Prover proofs can be cross-verified by Lean 4 (at reduced fidelity), and vice versa via future work.
  4. Peace Axiom #196 is a first-class structural invariant of the prover, not a documented convention.

What this paper explicitly does not claim

  • Rei-PL Prover is ready to replace Lean 4 in any workflow.
  • D-FUMT₈ semantics is philosophically-settled (it remains a research position of Rei-AIOS / 藤本, not a community consensus).
  • Full Mathlib can be ported (3-6 month work at Phase 2).
  • All Lean 4 limitations identified (see Part B) can be addressed by this or any single prover — some are genuinely hard research problems.

Part A. その回の証明 (Formal proofs)

A.1 VERIFIED

Core type (src/rei-pl-prover/types.ts):

export type DFumt8Value = 'TRUE' | 'FALSE' | 'BOTH' | 'NEITHER'
                        | 'INFINITY' | 'ZERO' | 'FLOWING' | 'SELF';

export type ProofTerm =
  | { tag: 'Axiom'; name: string; value: DFumt8Value; justification: string }
  | { tag: 'AndTable'; left: ProofTerm; right: ProofTerm }
  | { tag: 'OrTable'; left: ProofTerm; right: ProofTerm }
  | { tag: 'Refl'; value: DFumt8Value }
  | { tag: 'PeaceInvariant' }
  | { tag: 'Substitute'; premise: ProofTerm };

export interface Judgment {
  readonly claim: DFumt8Value;
  readonly proof: ProofTerm;
  readonly label?: string;
}
Enter fullscreen mode Exit fullscreen mode

Checker semantics (src/rei-pl-prover/checker.ts):

  • andOp(a, b) encodes the full 8×8 D-FUMT₈ AND truth table (preserving Belnap-4 classical core; ZERO absorbs; SELF propagates; FLOWING self-composes to FLOWING).
  • evaluate(term) reduces a proof term to its D-FUMT₈ value.
  • checkJudgment(j) runs evaluate(j.proof) and rejects the judgment if the result ≠ j.claim, enforcing Peace Axiom #196.

Three toy theorems:

// Theorem 1
export const peaceAxiomTheorem: Judgment = {
  claim: 'TRUE',
  proof: { tag: 'PeaceInvariant' },
  label: 'peaceAxiom196',
};

// Theorem 2
export const bothIdempotenceTheorem: Judgment = {
  claim: 'BOTH',
  proof: {
    tag: 'AndTable',
    left:  { tag: 'Axiom', name: 'bothLiteral-L', value: 'BOTH', justification: 'D-FUMT₈ literal' },
    right: { tag: 'Axiom', name: 'bothLiteral-R', value: 'BOTH', justification: 'D-FUMT₈ literal' },
  },
  label: 'bothIdempotence',
};

// Theorem 3
export const flowingSelfComposeTheorem: Judgment = {
  claim: 'FLOWING',
  proof: {
    tag: 'AndTable',
    left:  { tag: 'Axiom', name: 'flowingLiteral-L', value: 'FLOWING', justification: 'D-FUMT₈ literal' },
    right: { tag: 'Axiom', name: 'flowingLiteral-R', value: 'FLOWING', justification: 'D-FUMT₈ literal' },
  },
  label: 'flowingSelfCompose',
};
Enter fullscreen mode Exit fullscreen mode

All three pass checkJudgment: { valid: true, value: matches claim, reason: 'judgment verified' }.

A.2 EMPIRICAL (test results)

npx tsx test/step997-rei-pl-prover-test.ts → 16 passed, 0 failed:

  • 3 theorems × 2 assertions (valid + value matches claim) = 6 assertions
  • 2 Peace Axiom rejection assertions
  • 4 truth-table evaluation assertions (AND(BOTH,BOTH), AND(FLOWING,FLOWING), AND(ZERO,TRUE), AND(SELF,NEITHER))
  • 4 Lean 4 export assertions (substance, axiom presence, namespace, theorem export)

Wall-clock: < 0.5 seconds.

A.3 Lean 4 bridge verification

Exported file data/lean4-mathlib/CollatzRei/Step997ReiPLExport.lean (1,817 bytes):

  • 6 opaque Prop axioms for non-classical D-FUMT₈ values.
  • 4 inhabitation axioms (so witnesses can be constructed).
  • 3 theorems mirroring the Rei-PL judgments.
  • lake env lean CollatzRei/Step997ReiPLExport.lean → exit 0.

Part B. 今回の発見 (Findings)

B.1 Mathlib v4.27 gaps encountered this session

Paper 134 surveyed AI tooling; Papers 133/135 partial-formalized Erdős/self-reference. Through these, we concretely identified 12 distinct Mathlib v4.27 gaps:

# Gap Addressed by Paper 137?
1 GL modal logic / Löb's theorem Partially — Peace Axiom replaces one modal claim
2 Sylvester-Schur theorem (classical, absent) No — Lean 4 domain (Paper 133)
3 Legendre formula (p-adic valuation of n!) No
4 Hypergraph Ramsey growth No
5 Nash fixed-point (Kakutani) No
6 Paraconsistent logic Partially — BOTH is native
7 Quantum logic / orthomodular lattices Partially — captured via FLOWING-like partials
8 Cubical / HoTT computational univalence No
9 Lean 4 totality restriction on Y / self-reference Partially — SELF-value is native
10 Prop is 2-valued; no BOTH/NEITHER/FLOWING native YES — this is Paper 137's central contribution
11 Proof search not native No (neural integration is Paper 140+)
12 Structure field reduction edge cases No

Gaps #6, #7, #9, #10 are directly improved by Rei-PL Prover's native D-FUMT₈ semantics.

B.2 The Peace Axiom #196 invariant

In Lean 4, invariants are conventions enforced by reviewer discipline. In Rei-PL Prover v0.1, Peace Axiom #196 is checker-enforced: any proof term whose computed D-FUMT₈ value disagrees with the claimed value is rejected with an explicit CLAIM-VALUE MISMATCH error. The test suite includes a deliberate fraudulent claim (FALSE claim with PeaceInvariant proof) and verifies its rejection.

This is the first Rei-AIOS artifact where Peace Axiom is a structural invariant of the formal system itself, not just documentation.

B.3 Co-evolution demonstrated

The 1-way Lean 4 export proves that Rei-PL Prover can feed Lean 4 / Mathlib: each Rei-PL theorem exports as a Lean 4 theorem that compiles. The reverse direction (Lean 4 → Rei-PL Prover) is the Phase 2 Paper 138 direction. Two-way co-evolution is thus a 2-paper effort, not an insurmountable research problem.

Part C. 次の発明 (Next inventions)

  1. Phase 2 — Mathlib translation layer (~3 months). Auto-translate Lean 4 theorems to Rei-PL Prover with Prop → Prop8[TRUE] embedding. Target: 70% of Mathlib auto-ported.
  2. Phase 3 — Self-hosting (~6 months). Rei-PL Prover proves its own soundness (reflection principle). Paper 132 Part F.4 methodology applied internally.
  3. Phase 4 — Neural tactic search (~6 months). Integrate NNUE D-FUMT (already in Rei-AIOS Papers 199-210+) as a native tactic-suggester, not bolt-on.
  4. Phase 5 — Full co-evolution daemon (~1 year). Daily Mathlib pull + auto-translate + reverse-bridge back to Lean 4 for community contribution. Aligns with project_metadb_rei_aios_full_autosync_goal vision.

Part D. 次の未解決 (Next open problems)

  • Q65 (new, this paper): is the 8×8 D-FUMT₈ AND truth table the canonical 8-valued extension of 4-valued Belnap logic, or are there other equally-natural extensions? Uniqueness up to some equivalence is open.
  • Q66: Peace Axiom #196 is currently a single-bit invariant (TRUE unconditional). Can it be generalized to a Prop8-valued invariant that captures more subtle ethical structure, while remaining checker-enforceable?
  • Q67: Rei-PL Prover's Substitute rule is currently a no-op (just passes through the premise). What is the minimal useful set of substitution rules for a D-FUMT₈ proof term language? (Design question for v0.2.)
  • Q68: the Lean 4 export uses opaque Prop axioms for non-classical values. Is there a Lean 4 extension (or Mathlib PR) that could make this translation faithful rather than lossy?

Part E. 引用 (References)

  • Rei-AIOS STEP 406 (八値論理基盤) src/axiom-os/seven-logic.ts.
  • Belnap, N., A useful four-valued logic, 1977.
  • da Costa, N., Inconsistent formal systems, 1963.
  • Birkhoff, G. & von Neumann, J., The logic of quantum mechanics, Ann. Math. 37 (1936).
  • 龍樹 (Nāgārjuna), Mūlamadhyamakakārikā — catuṣkoṭi origin of 4-valued BOTH/NEITHER.
  • ヘラクレイトス — FLOWING (πάντα ῥεῖ) semantic source.
  • Gödel, K., Über formal unentscheidbare Sätze (SELF value source, self-reference).
  • Löb, M. H. (1955) — SELF value source.
  • Rei-AIOS Paper 130 (DOI 10.5281/zenodo.19700758), Paper 133 (DOI 10.5281/zenodo.19713219), Paper 134 (DOI 10.5281/zenodo.19709966).
  • Mathlib v4.27.0, Lean 4.27.0.
  • Peace Axiom #196 · 藤本伸樹 × Rei-AIOS.

Part F. 誠実な失敗と修正の記録 (Honest failures and corrections)

F.1 Lean 4 export initial draft failed to compile

First export used Classical.choice ⟨both_state, id⟩ syntax. Lean 4 rejected this: both_state is a Prop axiom (not an inductive type with a single constructor), so anonymous-constructor syntax doesn't apply.

Fix: added inhabitation axioms (axiom both_inhabited : both_state etc.) so proofs can construct witnesses without Classical.choice. Export now compiles under lake env lean exit 0.

Lesson: encoding opaque Props requires paired inhabitation axioms for constructive proof term expression. This is standard Lean 4 practice but easy to overlook in auto-generated output.

F.2 Test expectations inconsistent with refactored prelude

After updating the LEAN_PRELUDE to remove peace_axiom_196 axiom, a test assertion checking for that string failed. Updated test to check for both_inhabited (which is in the new prelude).

Lesson: test assertions that match string content are fragile to refactoring; future revision should test behavior (roundtrip build-verify) rather than content snippets.

F.3 Scope honesty — do not overstate

Early draft of this paper claimed "Rei-PL Prover surpasses Lean 4". This overstates: Rei-PL Prover v0.1 is 160 LOC with 3 theorems; Lean 4 + Mathlib is ~3 million LOC with 180,000 theorems. Current draft replaces overclaim with "complements Lean 4 by providing native D-FUMT₈ semantics" — accurate scope.

Lesson: framing newly-built tooling against mature tooling is prone to overclaim; honesty requires stating concrete capability + concrete scope gap.

Part G. テスト結果 (Tests) 

$ npx tsx test/step997-rei-pl-prover-test.ts

=== STEP 997 Rei-PL Prover v0.1 tests ===
[1/4] Three toy theorems pass checker: 6/6 ✓
[2/4] Peace Axiom #196 invariant rejects mismatched claim: 2/2 ✓
[3/4] Truth-table operations: 4/4 ✓
[4/4] Lean 4 export produces well-formed source: 4/4 ✓
=== STEP 997: 16 passed, 0 failed ===

$ cd data/lean4-mathlib && lake env lean CollatzRei/Step997ReiPLExport.lean
# exit 0 (no output)
Enter fullscreen mode Exit fullscreen mode

All 16 unit tests pass; Lean 4 round-trip verified.

Part H. データセット (Datasets — if applicable)

No META-DB entries modified. The Rei-PL Prover itself adds a new artifact class (not a problem), so it is referenced in future papers rather than entered in Open Problems META-DB.

Part I. 公開・再現手順 (Publication & reproducibility)

  • Zenodo DOI: (pending at publication time)
  • Internet Archive / Harvard Dataverse / 8 blog mirrors: standard 11-platform pipeline
  • Source code (AGPL-3.0): fc0web/rei-aios at commit (pending)
  • Key files:
    • src/rei-pl-prover/ (4 modules, ~160 LOC)
    • test/step997-rei-pl-prover-test.ts (16 tests)
    • data/rei-pl-prover/v0_1-export.lean (Lean 4 export)
    • data/lean4-mathlib/CollatzRei/Step997ReiPLExport.lean (Lean 4 build-verified copy)

Quickstart 

git clone https://github.com/fc0web/rei-aios.git
cd rei-aios
npm install
npx tsx test/step997-rei-pl-prover-test.ts  # run tests
cd data/lean4-mathlib
lake env lean CollatzRei/Step997ReiPLExport.lean  # verify bridge
Enter fullscreen mode Exit fullscreen mode

Part J. 限界 (Limitations)

  1. Scale: 160 LOC, 3 toy theorems. Far from Mathlib-level.
  2. No self-hosting: prover is TypeScript-based; doesn't prove itself (Phase 3).
  3. Lean 4 export is lossy: opaque axioms for non-classical values; round-trip fidelity limited.
  4. Proof search is manual: user constructs proof terms by hand; no neural / symbolic search integrated (Phase 4).
  5. No Mathlib-equivalent library: standard theorems (e.g., Peano arithmetic in D-FUMT₈) need to be built from scratch.
  6. D-FUMT₈ truth tables are not community-consensus semantics: they reflect Rei-AIOS's design choices (src/axiom-os/seven-logic.ts). Different designers may propose alternative 8-valued extensions.
  7. Peace Axiom #196 is a Rei-AIOS invariant, not a universal moral principle: its enforceability is structural, but its philosophical validity is outside formal verification scope.

Part K. 謝辞 (Acknowledgements)

  • Belnap / da Costa / Birkhoff-vN / 龍樹 / ヘラクレイトス / Gödel / Löb — the philosophical and logical lineage of 8-valued reasoning.
  • Lean 4 / Mathlib teams for the exceptional baseline against which Rei-PL Prover is measured.
  • Rei-AIOS STEP 406 八値論理基盤 (src/axiom-os/seven-logic.ts), Papers 133-135 methodology.
  • Peace Axiom #196 · Fujimoto, Nobuki (藤本 伸樹) × Rei-AIOS (Claude Opus 4.7).

End of Paper 137.

Top comments (0)