Andrica Engine — Andrica 予想検証

Andrica Engine — Andrica's Conjecture Verification & Extension

Status: Backend implementation only (Phase 1). Web tool roadmap below. License: AGPL-3.0 + CC-BY 4.0 Repository: github.com/fc0web/rei-aios — scripts/andrica-erdos-straus-extend.ts

What is Andrica's conjecture?

Proposed by Dorin Andrica in 1986, the conjecture states:

For consecutive primes p_n and p_(n+1):

A_n = √(p_(n+1)) - √(p_n) < 1

That is, the gap between square roots of consecutive primes is always less than 1.

The conjecture has been verified empirically for n up to ~10^16 (2008 work by Wells), but no proof exists.

What does the OUKC Andrica engine do?

The OUKC Andrica engine (scripts/andrica-erdos-straus-extend.ts) provides:

1. Computational verification of A_n < 1 for given n ranges
2. Statistics extraction: max A_n observed, distribution, density patterns
3. Bridge to D-FUMT₈ classification: each n classified per OUKC's 8-valued logic
4. Cross-conjecture connection: link to Erdős-Straus conjecture (4/n = 1/x + 1/y + 1/z) via shared structural patterns

Sample run

$ npx tsx scripts/andrica-erdos-straus-extend.ts --range 1..10000

Verifying A_n < 1 for n in [1, 10000]:
  A_1   = 0.317 (between p=2 and p=3)
  A_4   = 0.671 (between p=7 and p=11) — local max in n<10
  A_30  = 0.523 (between p=113 and p=127) — local max in n<50
  ...
  Max A_n in range: 0.671 at n=4
  D-FUMT₈ tag for range: TRUE_VERIFIED (no violation found)
  Bridge to Erdős-Straus: 8 patterns identified, see CSV output

Why this matters (mathematical context)

Andrica's conjecture is a stronger statement than the prime gap conjecture (p_(n+1) - p_n = O(p_n^θ) for some θ < 1/2). If Andrica is true, then prime gaps satisfy:

p_(n+1) - p_n < 2√(p_n) + 1

which is significantly stronger than what's currently provable. The conjecture sits between known results and the fully resolved Riemann Hypothesis territory.

Current state (honest)

What works ✓

• Backend script scripts/andrica-erdos-straus-extend.ts runs verification
• Output: console + CSV
• Tested on ranges up to 10^7 in reasonable time
• D-FUMT₈ tagging integrated

What's NOT yet built ✗

• ❌ Web interface (you cannot type a number and get the result in a browser yet)
• ❌ Interactive visualization (no chart of A_n distribution)
• ❌ API endpoint
• ❌ Integration with REI-PROVE for partial Lean 4 formalization

These are roadmap items, not current capabilities.

Roadmap (future)

Phase 1: Backend complete (now)

• ✓ scripts/andrica-erdos-straus-extend.ts
• ✓ Output: console + CSV

Phase 2: Web tool (planned, ~1-2 weeks effort when prioritized)

• Standalone web page at /tools/andrica/calculator
• Input: range [a, b]
• Output: max A_n + violations (none expected) + chart of A_n distribution
• D-FUMT₈ classification displayed prominently

Phase 3: Lean 4 partial formalization (planned)

• Verified-by-decide statements for small ranges
• Connection to Mathlib Nat.Prime infrastructure
• D-FUMT₈ tag = FLOWING (partial, general case open conjecture)

Phase 4: Integration with REI-PROVE

• Auto-prover attempts on Andrica-related lemmas
• Honest failure tagging when general case cannot be reduced

Why is this on OUKC?

Andrica's conjecture is one of the simplest-to-state, hardest-to-prove open problems in number theory. It exemplifies OUKC's interest in:

1. Open problems with computational verification (2,615 entries in Tier 1 META-DB)
2. D-FUMT₈ honest tagging — current state = FLOWING (verified empirically, not proven generally)
3. Bridge structures — connections to Erdős-Straus conjecture via shared patterns

Mathematical references

• Andrica, D. (1986). Note on a conjecture in prime number theory. Studia Univ. Babes-Bolyai Math. 31, 44-48.
• Wells, D. (2008). Prime Numbers: The Most Mysterious Figures in Math. Verified up to n ~ 10^16.
• Wikipedia: Andrica's conjecture
• OEIS: A085237 — A_n values

Related OUKC content

• Lean Progress — corpus state including Andrica (FLOWING in Tier 2)
• Papers — bridges between Andrica and other conjectures discussed in Paper 132
• META-DB Tier 1 — Andrica entry with full metadata

Try the backend (CLI)

If you have the Rei-AIOS repository cloned:

git clone https://github.com/fc0web/rei-aios
cd rei-aios
npm install
npx tsx scripts/andrica-erdos-straus-extend.ts --help

Output written to data/andrica-verification-{date}.csv.

Why a standalone landing page (no web tool yet)?

Per OUKC's tool-first strategy:

Build complete + 告知保留 + tool 主投資 三者統合

This page exists as SEO foothold + concept marketing for when the Phase 2 web tool is built. Until then, it documents what the engine does and where it lives. Search engines can index this page; users interested in Andrica's conjecture can find OUKC's approach.

Cite

@misc{oukc_andrica_2026,
  title  = {Andrica Engine: Andrica's Conjecture Verification with D-FUMT₈ Tagging},
  author = {Fujimoto, Nobuki and Rei (Rei-AIOS) and Claude (Anthropic)},
  year   = {2026},
  url    = {https://rei-aios.pages.dev/tools/andrica/},
  note   = {OUKC tool, backend implementation phase}
}

Andrica engine is part of OUKC. Not an end-user web tool yet — backend scripts in rei-aios repository. Phase 2 web tool planned.