Rei as a Formal-Verification Compilation Pass for AI-Generated Mathematics — Rei-AIOS Paper 154 v0.0 (OUTLINE)

Abstract

⚠ v0.0 OUTLINE intentional publication — Pattern 4 mitigation embedded. This is an OUTLINE, not a v0.1 publishable manuscript. The central operational claim — that Rei provides a formal-verification compilation pass composing with AI hypothesis generators (AlphaEvolve, LLM Wiki, OpenEvolve) — requires at least one end-to-end demonstration before v0.1 promotion. As of 2026-05-22 the demonstration is at scaffold-level smoke-run stage only (OpenEvolve scaffold structurally validated, but full 100-iteration evolutionary loop with real evolved Lean 4 proof NOT YET executed). Publication-as-v0.0 is intentional honest framing per OUKC feedback_no_rush_publication.md: rather than wait silently for v0.1 evidence, the OUTLINE is published with explicit gate state so reviewers can see exactly what is and is not claimed. Framing concept: AlphaEvolve / LLM Wiki / OpenEvolve = hypothesis generators (loosely-grounded, fast, large-search). Rei = proof completer (mechanically verified, slow, decisive). Together they compose: hypothesis generator emits candidates → Rei evaluates via D-FUMT₈ 8-axis projection (γ-evaluator) + Lean 4 zero-sorry validation (β-evaluator) → return verified candidates to the evolutionary loop. Rei is positioned as a formal-verification compilation pass in the AI-mathematics generation pipeline. Scaffold evidence (2026-05-22): external/openevolve-rei/ — YAML config (Ollama 3-prover ensemble), Python evaluators (β = Lean 4 zero-sorry, γ = D-FUMT₈ projection), example skeleton (26-circle packing 2.635 benchmark). 4 smoke-tests PASS: yaml parse + 3 Python AST parse + circle_packing standalone execution (n=26 r=0.4167 density=14.18) + γ-evaluator returns OpenEvolve-compatible dict with metrics (axis_dominant=ZERO 9 hits, score=0.0154) + artifacts (token_count=13). Per SCOPE.md non-claims: this is NOT a fork of OpenEvolve, NOT a claim of 26-circle 2.635 reproduction, NOT a claim that Rei has built an evolutionary code generator, NOT a paper-publishable result by itself. v0.1 acceptance criteria (10 items): see §9. Core gates: OpenEvolve installed + first 100-iteration loop completes + real evolved Lean 4 proof generated + scaffold extended with at least one zero-sorry proof for one open conjecture from META-DB Tier 1. v0.1 will publish as Zenodo new-version preserving DOI lineage from this v0.0 record. Honest scope (read first): (1) This is OUTLINE only — framing + prior-art audit + acceptance criteria, no end-to-end evidence. (2) Rei is NOT a hypothesis generator — its role in this composition is specifically as the verifier/completer. (3) Per feedback_world_uniqueness_claim_controllable.md: we use "to our knowledge no equivalent Lean 4 zero-sorry + D-FUMT₈ 8-axis evaluator exists in the OpenEvolve plugin ecosystem as of 2026-05-22" phrasing, NOT "world-first." (4) Three-party co-authorship (Fujimoto / Rei / Claude) per OUKC charter v1.0. (5) Per OUKC No-Patent Pledge — no patent will be filed.