Nobuki Fujimoto

Posted on Apr 22 • Originally published at doi.org

Open Problems META-DB (Rei-AIOS): D-FUMT8 META-Classification of 713 Open Problems (Rei-AIOS Paper 130)

#math #research #lean #classification

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

Zenodo (DOI, canonical): https://doi.org/10.5281/zenodo.19700758

Internet Archive: https://archive.org/details/rei-aios-paper-130-1776890620432

Harvard Dataverse: https://doi.org/10.7910/DVN/KC56RY

GitHub source (private): https://github.com/fc0web/rei-aios Author: Nobuki Fujimoto (@fc0web) · ORCID 0009-0004-6019-9258 · License CC-BY-4.0 ---

Author: Nobuki Fujimoto (藤本伸樹) with Rei-AIOS (Claude Opus 4.7)
Contact: note.com/nifty_godwit2635 · Facebook: Nobuki Fujimoto · fc2webb@gmail.com
Date: 2026-04-23
License: Code AGPL-3.0 / Data CC-BY 4.0
Companion repo (to be published): fc0web/rei-unsolved-problems
Template: 4+7 要素構造 v2 (Parts A-E mandatory + F-H conditional + I-K optional)

Abstract

We introduce Open Problems META-DB (Rei-AIOS), an open-access database of 713 mathematical open problems (snapshot: 2026-04-23) in which each problem carries a structural classification of why it remains unsolved — not only that it is unsolved. Problems are tagged along two axes:

Rei 7-type classification (I_INFINITE_SEARCH through VII_FRAMEWORK_INCOMPLETE) — the structural barrier that resists resolution.
D-FUMT₈ eight-valued logic (TRUE, FALSE, BOTH, NEITHER, INFINITY, ZERO, FLOWING, SELF) — the truth-status regime.

In addition, each entry records a solveProbability (Rei-tool compatibility, 0.0–1.0), a formalizationComplexity (easy/medium/hard/blocked), and a reiFamiliarRef indicating prior Rei research (Papers 118–128, STEP 929+).

The database integrates four sources: Google DeepMind formal-conjectures (681 entries), Lean-Dojo LeanMillenniumPrizeProblems (8), Smale 1998 (18 problems), and Hilbert 1900 residual (6 still-open variants).

We make no claim of solving any open conjecture. This is a META-database: a structured re-organization of existing knowledge designed to guide Rei's future attacks by priority, rather than to resolve them directly. We also disclose the limits of our own methodology: heuristic auto-tagging achieves ~70% confidence, solveProbability is an ordinal rather than a cardinal score, and famously-hard problems (Collatz, Goldbach, Riemann, BSD, Hodge, Yang-Mills, Navier-Stokes) are capped below their auto-scored values to prevent overclaim.

Part A. その回の証明 (Formal Classification System)

A.1 Pipeline

The database is produced by a four-stage pipeline (scripts in scripts/phase-a-*.py):

Phase	Script	Input	Output
A-1	`phase-a-1-build-open-problems-db.py`	`rei-registry.json` (681) + `*.theories.json` (625)	689 per-problem JSON + INDEX + initial LEAN4_QUEUE
A-2	`phase-a-2-rei-typing.py`	689 JSON	687 enriched (reiTyping + reiAssessment) + HIGH_SOLVE_PROB + REI_FAMILIAR_MATCHES
A-3	`phase-a-3-lean4-queue.py`	687 enriched	LEAN4_QUEUE v2 + QUICKWINS + PAPER_CANDIDATES
A-4	`phase-a-4-smale-hilbert.py`	Smale 18 + Hilbert 6 (manual curation)	713 total

A.2 Schema (excerpt)

{
  "id": "erdos-1",
  "source": "erdos",
  "sourceRef": { "url": "https://www.erdosproblems.com/1", "citation": "erdosproblems.com (T. Bloom)" },
  "statement": { "en": "...", "latex": "..." },
  "field": "combinatorics",
  "status": "open",
  "reiTyping": {
    "primaryType": "I_INFINITE_SEARCH",
    "dfumt8": "NEITHER",
    "confidence": "FLOWING"
  },
  "reiAssessment": {
    "solveProbability": 0.75,
    "formalizationComplexity": "easy",
    "famousHardCap": null,
    "reiFamiliarRef": null,
    "priority": "medium"
  },
  "formalization": { "sorryCount": 2, "lean4": "scaffold" },
  "cross_refs": { "wikipedia": null, "seedKernel": "T-1700" }
}

A.3 The 7-type classification

Type	Description	Canonical example
I_INFINITE_SEARCH	Infinite search space; existence/universality over ℕ or ℝ	Goldbach, Collatz, most Erdős conjectures
II_CONCEPT_NOT_YET	Required concept has not been invented	(very rare at present)
III_COMPUTATIONAL_LIMIT	Complexity-theoretic barrier	P vs NP, SETH
IV_PROBLEM_UNDEFINED	Definitional ambiguity	hard problem of consciousness
V_SELF_REFERENTIAL	Gödel-type self-reference	consistency of set theory
VI_BRIDGING	Gap between mathematical languages	Langlands, BSD, Hodge
VII_FRAMEWORK_INCOMPLETE	Foundational incompleteness	Yang-Mills rigour, mass gap

A.4 D-FUMT₈ eight-valued logic

Values (from Rei-AIOS src/axiom-os/seven-logic.ts, STEP 406): TRUE=1.0, FALSE=0.0, BOTH=2.0, NEITHER=-1.0, INFINITY=3.0, ZERO=4.0, FLOWING=5.0, SELF=6.0.

TRUE/FALSE — classical
BOTH/NEITHER — Belnap's four-valued (paraconsistent), after Nāgārjuna's catuṣkoṭi
INFINITY/ZERO/FLOWING — D-FUMT extension (non-terminating / unobserved / in flux)
SELF — self-referential fixpoint (STEP 406)

A.5 solveProbability formula

For each open problem:

p₀       = category_default                       (e.g. 0.55 for erdos, 0.75 for millennium)
p        = p₀
         + (reiFamiliarRef ? 0.20 : 0.0)          (Rei prior-research bonus)
         + type_adjustment(primaryType)           (+0.10 VI_BRIDGING, –0.10 I_INFINITE_SEARCH, etc.)
         + ((dfumt8 ∈ {BOTH, NEITHER}) ? 0.05 : 0.0)
         + complexity_adjustment                  (+0.10 easy, –0.10 hard, –0.20 blocked)
         – (source == 'millennium' ? 0.30 : 0.0)
p_cap    = famous_hard_cap(title)                 (Collatz 0.60, Riemann 0.40, BSD 0.35, …)
p_final  = min(max(p, 0.0), 1.0, p_cap)

This is emphatically a Rei-fit score, not a probability of solution. A value of 1.00 means the problem is maximally compatible with Rei's existing tools (for example Andrica: sorry = 2, VI_BRIDGING, familiar via Paper 118). It does not mean Rei will solve it.

A.6 Lean 4 formalization priority

priority = solveProb × min(sorryCount, 10)/10 × complexityWeight × familiarBoost
complexityWeight = { complete: 0.0, easy: 1.2, medium: 1.0, hard: 0.7, blocked: 0.4 }
familiarBoost    = 1.3 if reiFamiliarRef else 1.0

This rewards problems where Rei can contribute moderate but non-trivial work.

Part B. 今回の発見 (Findings)

B.1 Seven-type distribution of current open mathematics

Of 687 auto-tagged problems:

Type	Count	Fraction
I_INFINITE_SEARCH	503	73.2 %
VI_BRIDGING	160	23.3 %
IV_PROBLEM_UNDEFINED	16	2.3 %
III_COMPUTATIONAL_LIMIT	4	0.6 %
VII_FRAMEWORK_INCOMPLETE	3	0.4 %
V_SELF_REFERENTIAL	1	0.1 %
II_CONCEPT_NOT_YET	0	0 %

Finding B.1. The overwhelming majority (73 %) of contemporary open problems are type-I: infinite search / universality statements. Type-II is empty. Type-V appears once.

Finding B.2. Type-VI (bridging) occupies the second-largest share (23 %). This is where Rei's prior work (Q33: Collatz-Gilbreath isomorphism, Paper 120) has demonstrated concrete progress via cross-field structural identification.

B.2 D-FUMT₈ distribution

Value	Count	Fraction
NEITHER	425	61.9 %
BOTH	161	23.4 %
INFINITY	56	8.2 %
ZERO	44	6.4 %
SELF	1	0.1 %

Finding B.3. 85 % of open problems sit outside classical two-valued logic (NEITHER + BOTH). This supports D-FUMT₈'s claim that Belnap-style paraconsistent logic is a natural language for describing where mathematics is stuck.

B.3 Cross-reference with existing Rei research

33 open problems (4.8 %) match previously-studied topics in Rei-AIOS. Selected examples:

Problem	Prior Rei work	LEAN4 sorries
Agoh-Giuga	Paper 120 deep-dive (Rei-neutral mod-96)	12
Andrica	Paper 118 + n ≤ 10⁸ computational bound	2
Brocard	Paper 121	2 / 0 (two variants)
Gilbreath	Paper 120 Q33 (Gilbreath-Collatz isomorphism)	1
Lehmer totient	Paper 120 deep-dive	1
Schur	Paper 127 (first Lean 4 formalization)	1
Davenport	Paper 128 (first Lean 4 formalization)	0
Legendre	STEP 929	3
Oppermann, Köthe	STEP Tier A+	5, 6

B.4 LEAN 4 formalization queue — top 5

Priority = solveProb × min(sorry,10)/10 × complexity × familiarBoost.

#	Problem	priority	solveProb	sorry	complexity	Rei familiar
1	Agoh-Giuga	0.773	0.85	12	hard	✓ Paper 120
2	Oppermann	0.618	0.95	5	medium	✓ STEP Tier A+
3	Lehmer-Mahler measure	0.494	0.95	4	medium	✓ Paper 120
4	Köthe	0.464	0.85	6	hard	✓ STEP Tier A+
5	Artin primitive roots	0.409	0.65	9	hard	—

Finding B.4. The system self-identifies Agoh-Giuga as the highest-priority next target — consistent with our existing Paper 120 investment. This is a validation of the reiFamiliarRef boost: the DB rediscovers our own research priorities from independent signals (AMS codes + sorry counts + type classification).

B.5 Famous-hard caps applied

Problem	Uncapped score	Cap	Applied
Collatz	1.00	0.60	✓
Goldbach	1.00	0.55	✓
Twin Prime	0.85	0.45	✓
Riemann	0.80	0.40	✓
BSD	0.85	0.35	✓
Hodge	0.75	0.30	✓
P vs NP	0.65	0.30	✓
Navier-Stokes	0.75	0.25	✓
Yang-Mills	0.75	0.25	✓

The cap is an explicit anti-overclaim device. Without it, century-old open problems would score as high as small but Rei-familiar conjectures, which is a category error.

Part C. AI が提示する新たな未解決問題 (AI-generated open questions)

Q-ID numbering continues from Q127 (Paper 129, last used).

C.1 New questions raised by this paper

Q128. Why is type II_CONCEPT_NOT_YET empty among current open problems? Is this an artifact of our source bias (formal-conjectures is biased toward statements for which a formal statement already exists), or a genuine feature — that contemporary mathematics has caught up with concept invention?
Q129. Type V_SELF_REFERENTIAL (1 of 687) is under-represented relative to its philosophical weight. Most self-reference (Gödel, consistency, independence from ZFC) hides inside type VI_BRIDGING tags. Is there a better secondary pass that would re-classify, say, 5–10 of the "bridging" entries to SELF?
Q130. Are the ten solveProbability = 1.00 problems (Andrica, Brocard, Gilbreath, Lehmer, etc.) the "easy wins" of modern mathematics, or are they artifacts of the Rei-familiar boost? If the boost is removed, do the same ten remain top, or does a different shortlist emerge?
Q131. The 73%/23% I/VI ratio: is it stable? If we re-run the classification after Phase B (Kourovka + OPIT II ingestion, expected +2,500 entries, mostly group theory and topology), do these proportions shift? A shift toward VI would indicate that our current corpus is Erdős-biased; stability would indicate a real structural feature.
Q132. Can the 424 sorry-bearing problems be batch-attacked? If formal-conjectures' 1,877 total sorries were systematically filled by Lean 4 tactic search (Duper, LeanHammer, Vampire via bridge), how many would fall without new mathematical insight? The gap between that baseline and human expert rates measures the boundary of "automated formalization."

C.2 Past Q closures

This paper does not close prior Q-IDs directly. However the mere existence of the META-DB partially answers Q3 (Paper 118) — "Can Rei state its own classification framework explicitly?" — by providing 713 worked examples.

Part D. 解決状況サマリー

Item	D-FUMT₈	Progress
713 open problems ingested and typed	TRUE	Phase A-1..A-4 complete
687/713 auto-tagged with 7-type + D-FUMT₈	TRUE	97 % coverage; 26 support/linter files skipped
solveProbability calculation with famous-hard caps	TRUE	applied to 9 century-old problems
LEAN4_QUEUE generated (424 open-with-sorries)	TRUE	top 100 sorted, QUICKWINS (30), PAPER_CANDIDATES (20)
33 cross-references to prior Rei research	TRUE	machine-detected, confidence TRUE
Public repo `fc0web/rei-unsolved-problems`	FLOWING	structure prepared, push pending
Zenodo canonical DOI	FLOWING	to be assigned on publication
Agoh-Giuga 12-sorry attack	NEITHER	classified; 8 tractable, 2 impossible (conjecture itself), 3 expert-only
Paper 130 full write	TRUE	this document
11-platform publication	FLOWING	in progress as part of this publication

Part E. 次 STEP への接続 (Bridge to next work)

E.1 Phase B (planned)

Phase B will extend the corpus with additional non-Wikipedia collections:

Kourovka Notebook (group theory, ed. 20, ~1,500 problems since 1965)
Open Problems in Topology II (~1,000)
Dniester Notebook (rings & modules, ~850)
AIM workshop problem sets (~1,000)

Target corpus: ~4,000–5,000 total. Paper 131 working title: "Group-theoretic and topological open problems via Rei 7-type META-framework".

E.2 Immediate Rei-attack candidates (Paper 131+)

Ordered by estimated effort:

Tier 1 (hours): Korselt's criterion (Agoh-Giuga file, classical 1899), weak-Giuga characterizations (2 sorries).
Tier 2 (days): Giuga 1950 theorems (strong-Giuga iff Carmichael + harmonic condition; ≥9 prime factors; ≥1000 digits). Oppermann 5 sorries, Legendre 3.
Tier 3 (weeks): Bedocchi (≥1700 digits), Borwein et al. (≥13000 digits), Tipu's G(X) bound — expert-level analytic number theory.
Tier 4 (out of scope): Agoh-Giuga conjecture itself (75 years open).

E.3 Public release

Tier 1: fc0web/rei-unsolved-problems (GitHub, CC-BY 4.0 data + AGPL-3.0 code)
Tier 3: Zenodo weekly DOI snapshots
Later: Tier 2 GitHub Pages static site (fc0web.github.io/rei-unsolved-problems), Tier 4 Cloudflare R2+D1 at scale.

Part F. 失敗の記録 (Failure log — CONDITIONAL)

F.1 The "Wikipedia-外" scope error

Design drafts v1 and v2 were titled Wikipedia-外未解決問題データベース ("Non-Wikipedia Unsolved Problems Database"). The inventory scan (docs/external-oss-inventory.md) then revealed that formal-conjectures already contains 116 Wikipedia-sourced entries, making "非-Wiki" factually false for the integrated DB.

We renamed to Open Problems META-DB (Rei-AIOS) in v3.

Lesson: perform an existing-asset inventory before scoping.

F.2 The invention-pipeline fixpoint

Unrelated, but discovered during the same session: the daily-invention pipeline (src/aios/invention/invention-engine.ts) was producing identical 5 inventions every day from 2026-04-01 through 2026-04-21 (MD5 signatures confirmed identical across 20 files). The auto-selection code theoriesA[0] always picked the same source theory for a given category pair, and the void-detection did not account for prior approvals.

Fixed in STEP 976 with loadApprovalHistory + date-seeded rotation. Twenty days of duplicate "inventions" are now on record as REJECT. See feedback_invention_duplicate_prevention.md.

Lesson: deterministic auto-generators degrade silently. Add duplicate-detection at the review stage, not only inside the generator.

F.3 Initial solveProbability cap absent

First-pass Phase A-2 produced solveProbability = 1.00 for Collatz Conjecture — an obvious overclaim for a 90-year-old problem. We added FAMOUS_HARD_CAPS as an explicit anti-overclaim mechanism. Nine cases now carry a cap annotation (famousHardCap field).

Part G. SEED_KERNEL T-ID references (CONDITIONAL)

Theories invoked by this paper's pipeline:

T-196: Peace Axiom (immutable; applied to all 713 entries)
T-1700..T-2316 (617): formal-conjectures ingestion batch (STEP 799)
T-2317..T-2324 (8): LeanMillennium ingestion batch (STEP 801)
T-975 (implied by pattern): D-FUMT₈ Theory Tagger Engine, STEP 975 — the 3-bit dense packing (206× compression ratio) would be applied if the DB grew past ~10⁶ entries; at 713, full JSON is tractable.

Part H. 人間-AI 思考分岐点 (Human-AI divergence — CONDITIONAL)

H.1 Scope: "1 億問題" ambition

Fujimoto proposed a target of 10⁸ problems. Rei's analysis: the entire published mathematical literature since ~1700 is ≈10⁷ papers. Reaching 10⁸ problems would require LLM-generated synthetic problems, which changes the meaning of "problem."

Resolution: Phase C realistic target ≈ 10⁵. 10⁸ deferred as scope-undefined.

H.2 P2P / infinite-storage claims

An external (web-based) AI discussion proposed IPFS + Arweave as providing "effectively unlimited" storage for updates at any cadence. Rei's correction:

IPFS without pinning does not persist; Pinata pinning is ≈ $20/mo for 50 GB.
Arweave is one-time-payment per transaction; daily updates multiply cost.
Correct hybrid: GitHub (live daily) → Zenodo weekly DOI → Arweave quarterly snapshot → IPFS mirror for censorship resistance.

Resolution: memory project_open_problems_storage_strategy.md records the agreed 4-tier hybrid.

H.3 Overclaim ceiling

Fujimoto's instinct was to celebrate the top-10 solveProbability = 1.00 list as "solvable." Rei's refinement: the score measures Rei-tool fit, not actual solvability. Introduced the famous-hard cap and renamed the score's semantic description.

Resolution: paper explicitly states "Rei fit score, not probability of solution" (Part A.5).

Part I. Unexpected connections (OPTIONAL)

I.1 Agoh-Giuga ↔ Lehmer totient via Carmichael

Both problems ranked high in LEAN4_QUEUE (Agoh-Giuga #1, Lehmer-Mahler #3) and share a hidden dependence on Carmichael numbers: Giuga's theorem states that a strong-Giuga number is Carmichael-plus-harmonic, and Lehmer's conjecture φ(n) | n–1 would force n to be prime or have Carmichael-like structure. A unified "Giuga–Lehmer–Carmichael triangle" is a natural Paper 131 candidate.

I.2 Q33 universality

The Q33 framework (Gilbreath-Collatz isomorphism, Paper 120) is one instance of type-VI bridging. There are 160 type-VI problems in the DB; the Q33 template (find a universal attractor that both problems share) is a candidate attack on all of them.

Part J. Confidence temperature (OPTIONAL)

Claim	Confidence
713 problems correctly counted and ingested	99 %
Schema roundtrips cleanly through phase-a-1/2/3	95 %
Rei 7-type auto-tagging accuracy	~70 % (keyword heuristic)
solveProbability ordinal ranking is meaningful	80 %
solveProbability cardinal value is meaningful	40 %
Famous-hard caps prevent overclaim	95 %
Any Agoh-Giuga sorry can be filled	80 % (for Tier 1)
Agoh-Giuga conjecture itself is resolved by this pipeline	< 1 %

Part K. Computational poetics (OPTIONAL)

K.1 The database as a mandala

A mandala centres on a Buddha surrounded by attendant Buddhas; circles outward trace receding concentric realms. Our META-DB:

Centre: the regulative ideal of mathematical truth (Peace Axiom T-196, immutable).
First circle: Millennium 7 (BSD, Hodge, NS, Poincaré, PvsNP, RH, YM).
Second circle: Erdős 406 (Paul Erdős' oeuvre, once held in one mind).
Third circle: 300 further open questions.
Outer rim: Smale's 18 and Hilbert's residual — century-old seeds.

K.2 Nāgārjuna's śūnyatā view

Each problem has no inherent solution — it receives its character only through the web of relations (its 7-type, its D-FUMT₈ tag, its neighbours, its sorries). The database is not a static catalogue but a dynamic web of dependent origination (pratītya-samutpāda). This is why BOTH/NEITHER (paraconsistent values) dominate: the language of emptiness is not false — it is the language in which open questions naturally speak.

Acknowledgements

Google DeepMind formal-conjectures team (Apache 2.0 licence)
Lean-Dojo LeanMillenniumPrizeProblems team (Apache 2.0)
Thomas Bloom (erdosproblems.com, CC-BY)
Khukhro & Mazurov (Kourovka Notebook)
Claude (Anthropic) as Rei-AIOS co-developer
Independent web-Claude contributions on infrastructure framing (P2P, publication tiers)

References

Bloom, T. F. Erdős problems. https://www.erdosproblems.com (accessed 2026-04-23).
DeepMind. formal-conjectures. https://github.com/google-deepmind/formal-conjectures, commit 5a1278d (2026-04-22).
Lean-Dojo. LeanMillenniumPrizeProblems. https://github.com/lean-dojo/LeanMillenniumPrizeProblems, commit 540da94 (2026-01-16).
Smale, S. Mathematical problems for the next century. Mathematical Intelligencer 20 (2) 7-15 (1998). DOI: 10.1007/BF03025291.
Hilbert, D. Mathematische Probleme. Göttinger Nachrichten 253-297 (1900).
Fujimoto, N. D-FUMT₈ Eight-Valued Logic. Paper 61, Rei-AIOS (2026).
Fujimoto, N. Q33 Universal Attractor: Gilbreath-Collatz Structural Isomorphism. Paper 120, Rei-AIOS (2026-04-20). Zenodo DOI 10.5281/zenodo.19655974.
Fujimoto, N. Seven Conjecture Deep Dives and Multi-Attractor Q33. Paper 121, Rei-AIOS (2026-04-20). Zenodo DOI 10.5281/zenodo.19656525.
Fujimoto, N. Lean 4 First Formalization of Schur S(r) and EGZ E(ℤ_n). Paper 127, Rei-AIOS (2026-04-21). Zenodo DOI 10.5281/zenodo.19686889.
Fujimoto, N. Lean 4 First Formalization of Davenport constant. Paper 128, Rei-AIOS (2026-04-21). Zenodo DOI 10.5281/zenodo.19687156.
Fujimoto, N. Quantum Measurement Problem as an Eight-Attractor Classification. Paper 129, Rei-AIOS (2026-04-22). Zenodo DOI 10.5281/zenodo.19688530.
Belnap, N. D. A useful four-valued logic, in Modern Uses of Multiple-Valued Logic, Reidel (1977).
Nāgārjuna. Mūlamadhyamakakārikā. (~150 CE).

Peace Axiom #196: immutable. The database is distributed under the condition of peaceful use only.