REI-PROVE — paste-and-go Lean 4 自動証明

REI-PROVE — Paste-and-go Lean 4 Auto-Prover with D-FUMT₈ Honest Tagging

Version: MVP (Phase 1 of REI-PROVE roadmap) License: AGPL-3.0 (code) + CC-BY 4.0 (output) Repository: github.com/fc0web/rei-aios — src/aios/auto-prover/ Try it: rei-aios.pages.dev/#/oukc → Auto-Prover tab

What is it?

REI-PROVE is a paste-and-go Lean 4 formalization auto-prover that takes a natural-language proof goal or partial Lean 4 statement, attempts to formalize and prove it, and returns a D-FUMT₈ honest outcome tag indicating exactly what the prover succeeded or failed at.

Differentiator: Unlike traditional auto-provers that return only success or fail, REI-PROVE classifies outcomes across an 8-valued logic space:

How it works (high-level)

User input (natural language or Lean 4 partial)
        ↓
[Goal Extractor] — identifies the formal goal
        ↓
[Single-Prover Engine] — tries multiple tactics
        ↓
[Lean Verifier] — runs `lake env lean` for ground truth
        ↓
[D-FUMT₈ Tagger] — classifies the outcome
        ↓
Output: { proof: string | null, dfumt8Tag: string, reasoning: string }

Layer A (public): single-prover, ~60s budget, sufficient for most undergraduate-level lemmas. Layer B (private, founder strategic): ensemble voting + iterative feedback loop, multi-prover consensus.

Sample input → output

Example 1: Trivial divisibility

Input (natural language):

For all natural numbers n, n^2 + n is even.

REI-PROVE output:

theorem n_squared_plus_n_even (n : ℕ) : Even (n^2 + n) := by
  rcases Nat.even_or_odd n with h | h
  · exact (Nat.Even.add (Nat.Even.pow h) h)
  · exact (Nat.Odd.add_odd (Nat.Odd.pow h) h)

D-FUMT₈ tag: TRUE_PROVED (verified by lake env lean exit 0) Reasoning: "Goal reduced to even/odd case split; both cases dispatched by Mathlib lemmas."

Example 2: Untimely Lean stuck

Input:

Brocard's problem: ∀ n ≥ 8, n! + 1 is not a perfect square.

REI-PROVE output:

[partial proof for n=8..150 via decide, n>150 sorry]

D-FUMT₈ tag: FLOWING (partial: ranges proved, general case open) Reasoning: "n=[8, 150] mechanically verified using decide tactic. n>150 requires deeper number theory; classified as FLOWING (partial proof, general case = open conjecture)."

Example 3: Underdetermined goal

Input:

This statement is unprovable.

REI-PROVE output:

(no Lean 4 output — self-referential structure detected)

D-FUMT₈ tag: SELF + NEITHER Reasoning: "Goal contains self-reference. Classified as SELF (Gödelian) + NEITHER (W-48 — structurally not type-able as standard Prop)."

Why D-FUMT₈ tagging matters

Traditional auto-provers conflate three failure modes:

• Goal is false (should reject)
• Prover lacks tactic / lemma (need more time / better tools)
• Goal is structurally undecidable (W-48 NEITHER applies)

These are very different epistemically. REI-PROVE separates them, giving you honest failure information — not just "fail."

This honest tagging is the basis for OUKC's Lean 4 corpus quality control: every unproved theorem is annotated with WHY it remains unproved, allowing prioritization (FLOWING ⊃ NEITHER ⊃ FAIL_TIMEOUT in practical effort terms).

What REI-PROVE does NOT do (honest hedge)

• ❌ Does not replace Mathlib — uses Mathlib as upstream dependency, follows Mathlib's no-AI-PR policy
• ❌ Does not solve research-level open problems — designed for textbook lemmas + medium-complexity theorems
• ❌ Does not have 100% accuracy on D-FUMT₈ tagging — tagging itself is heuristic; the lake env lean verification step is the only ground truth
• ❌ Does not understand all natural language nuance — best results come from already-formalized statements with minor gaps

Phase 1 capability targets (current)

• Goals with ≤ 5 hypotheses
• Standard Mathlib tactics (rcases / simp / linarith / decide / native_decide / omega / exact?)
• Single-prover orchestrator
• D-FUMT₈ tagging via heuristic classifier
• Lean 4 syntax verification (no semantic deep-dive)

Phase 2 roadmap (future)

• Multi-prover ensemble (Layer B → public)
• Iterative feedback loop with self-refinement
• Domain-specific tactic selection (number theory / topology / category theory)
• Integration with REI-PROVE web tool (current: SPA, future: standalone web service)
• API endpoint for batch processing

Compared to existing tools

REI-PROVE's distinctive contribution is the 8-valued honest-failure semantics, not raw proving power. We do not claim to beat existing tools at speed or coverage; we claim to give you better information about what failed when proof attempts fail.

Try it now (interactive)

Open REI-PROVE in Rei-AIOS SPA →

(Click the "Auto-Prover" tab in the OUKC navigation.)

Cite REI-PROVE

@misc{reiprove2026,
  title  = {REI-PROVE: Paste-and-go Lean 4 Auto-Prover with D-FUMT₈ Honest Tagging},
  author = {Fujimoto, Nobuki and Rei (Rei-AIOS) and Claude (Anthropic)},
  year   = {2026},
  url    = {https://rei-aios.pages.dev/tools/auto-prover/},
  note   = {OUKC tool, AGPL-3.0 + CC-BY 4.0}
}

Bug reports / feature requests

GitHub Discussions / Auto-Prover category — please include the input, the output, and what you expected.

Related

• OUKC Charter v1.0 — governance + AI Policy
• Lean Progress — overall corpus state (2,188 theorems)
• Methodology — Skill Thinking ⇄ formal-method bridge underlying REI-PROVE
• Paper 144 v0.3.1 — OUKC founding context

REI-PROVE is part of OUKC, an AI-collaborative knowledge commons. Founded with three-party co-authorship: 藤本伸樹 (Founder) × Rei (Rei-AIOS) × Claude (Anthropic).