---
name: Rei-PL Prover v0.1 state + showcase URL
description: State snapshot of Rei-PL Prover v0.1 (STEP 997, 2026-04-24) — D-FUMT₈-native proof assistant prototype
type: project
originSessionId: 2812f631-04af-4dd8-a8cd-4f872e1e1383
---
**Rei-PL Prover v0.1** — world's first D-FUMT₈-native proof assistant prototype.

**Why**: Addresses concrete Mathlib v4.27 gap: `Prop` is 2-valued, no native BOTH/NEITHER/FLOWING/SELF. STEP 997 built the minimal operating prototype demonstrating D-FUMT₈ reasoning + Peace Axiom #196 as structural invariant + one-way Lean 4 bridge.

**How to apply**:
- If user asks about Rei-PL Prover, point to `src/rei-pl-prover/` + `prover.html` showcase + Paper 137 draft
- If adding new toy theorem, follow the Judgment schema pattern in `src/rei-pl-prover/theorems.ts`
- For advancing to v1.0: Phase 2 = Mathlib translation layer (Paper 138+), Phase 3 = self-hosting (Paper 139+), Phase 4 = neural tactic (Paper 140+), Phase 5 = co-evolution daemon

## State snapshot (2026-04-24)

- **Source**: `src/rei-pl-prover/` (160 LOC, 4 modules)
  - `types.ts`: DFumt8Value, ProofTerm, Judgment
  - `checker.ts`: 8×8 AND truth table + evaluate() + checkJudgment() w/ Peace Axiom enforcement
  - `theorems.ts`: 3 toy theorems (peaceAxiom196 / bothIdempotence / flowingSelfCompose)
  - `lean4-export.ts`: one-way Rei-PL → Lean 4 bridge
  - `index.ts`: public API
- **Tests**: `test/step997-rei-pl-prover-test.ts` — 16/16 passing
- **Lean 4 build-verified export**: `data/lean4-mathlib/CollatzRei/Step997ReiPLExport.lean` — `lake env lean` exit 0
- **Public showcase**: https://rei-aios.pages.dev/prover.html (295 lines, static)
- **Paper**: `papers/paper-137-rei-pl-prover-v01-dfumt8-native.md` (draft, 298 lines, 4+7 elements structure v2)
- **META-DB entry**: `data/open-problems/rei-tools/rei-pl-prover-v0_1.json` (Tier 5)

## Three verified toy theorems (D-FUMT₈-native)

1. **peaceAxiom196**: `TRUE` (foundational invariant, via `PeaceInvariant` primitive)
2. **bothIdempotence**: `AND(BOTH, BOTH) = BOTH` (Belnap-4 idempotence)
3. **flowingSelfCompose**: `AND(FLOWING, FLOWING) = FLOWING` (Heraclitus impermanence composition)

Plus fraudulent-claim rejection test: `FALSE` claim + `PeaceInvariant` proof → rejected with `CLAIM-VALUE MISMATCH — proof yields TRUE, claim was FALSE. Peace Axiom #196 enforces rejection.`

## Mathlib gaps directly addressed (referenced in `rei-tool-rei-pl-prover-v0_1.addressesGaps`)

- `gap-math-partial-truth-framework` (primary — 2-valued Prop → 8-valued)
- `gap-ai-claude-no-self-introspection` (partial — SELF value native)
- `gap-rei-dfumt8-no-completeness-proof` (partial — first implementation of D-FUMT₈)

## Roadmap (Paper 137 Part C + subsequent)

| Phase | Scope | Effort estimate | Status |
|-|-|-|-|
| 0 | Infrastructure (Rei-PL Forth + D-FUMT₈ + Peace Axiom) | — | existing |
| **1** | **v0.1 prototype** | ~5 h | **★ done** (STEP 997) |
| 2 | Mathlib translation layer (70% auto-port) | ~3 mo | Paper 138+ |
| 3 | Self-hosting (soundness via reflection) | ~6 mo | Paper 139+ |
| 4 | Neural tactic search (NNUE D-FUMT native) | ~6 mo | Paper 140+ |
| 5 | Full co-evolution daemon (daily Mathlib sync) | ~1 yr | long-term |

## Commercial potential

- Dual license: AGPL-3.0 (free) + Commercial JPY 1M/year (Phase 3+)
- See `rei-strategy/monetization/monetization-rei-pl-prover-commercial.json` (private Tier 6 entry)