# Unsolved Hard Problems — RRC Strategic Path Forward **Date:** 2026-06-20 **Scope:** What to do with the RRC manifold/projection survey of 67 unsolved hard problems plus one solved boundary marker. **Claim boundary:** This document is strategic planning material. It proposes concrete next steps but does not claim any problem is solved or that any option will succeed. --- ## Executive Summary - The survey records **68 problem records** (67 unsolved, 1 solved boundary), assigned to **10 alignment clusters** and a 30x30 crossing matrix that encodes known reduction/shared-topic weights. - Most problems map to four RRC shape classes: `ProjectableGeometryTopology`, `CognitiveLoadField`, `LogogramProjection`, and `BurgersRGSolver`. The lone `ACCEPT` is the 3D Poincare conjecture, which validates that the `LeanTheoremReceipt` boundary can in principle be reached. - The clusters with the densest internal crossing structure are `cluster_02` (complexity core, 17 problems) and `cluster_04` (arithmetic/Diophantine, 16 problems). These are the highest-leverage targets for formalization scaffolding and attack-graph analysis. - The survey is currently **projection-only**: every entry is a `CANDIDATE` or `HOLD`. No entry has been promoted to `ACCEPT` by the RRC pipeline. - The 30x30 crossing matrix is the most actionable artifact beyond the clusters; it can be used directly to rank problems by centrality, reduction cascades, and braid-strand coverage. --- ## Strategic Options ### Option A: Convert the top N problems into Lean formalization stubs Produce Lean 4 modules in `0-Core-Formalism/lean/Semantics/Semantics/RRC/UnsolvedProblems/` that state each selected problem as a `def` or `theorem` with the exact RRC axes and status embedded as metadata. - **Pros:** Keeps Lean as the source of truth; stubs can be `#eval`-checked for syntactic well-formedness; creates a formal target surface for future proof work. - **Cons:** Stating a famous open problem in Lean adds no new mathematics; without a realistic path to proof, stubs risk becoming permanently `sorry`-laden unless quarantined. - **Effort:** Low for stubs, high if we demand `#eval` witnesses and no `sorry`. 1-2 days for 5-10 carefully chosen problems; a full 67-problem module would take several weeks and require quarantine discipline. **Recommended initial target set (5):** Riemann Hypothesis, P vs NP, Navier-Stokes existence, abc conjecture, Smooth 4D Poincare conjecture. These span the four dominant shape classes and have the strongest projection_declared scores. ### Option B: Use the crossing matrix to build an attack graph Treat the 30x30 crossing matrix as a weighted directed graph and compute node centrality, sink/source structure, and reduction cascades. Use the result to decide which problems are "hubs" and which are "leaves" that collapse if the hub is solved. - **Pros:** Directly leverages an existing artifact; gives an objective ordering; aligns with RRC's braid/crossing vocabulary (each edge is a crossing weight). - **Cons:** Weights are manually assigned and should not be treated as quantitative evidence; graph centrality can be gamed by over-connected underspecified problems (e.g., `quantum_gravity`). - **Effort:** 1-3 days for a Python shim that reads the JSON, builds the graph, and emits a ranked `attack_graph_receipt.json`. Could be reused by `rrc_refactor_oracle.py`. ### Option C: Promote alignment clusters into RRC shape classes and update the pipeline Merge the 10 alignment clusters into the existing RRC taxonomy used by `rrc_ray_tagger.py` and `docs/rrc_equation_classification.md`. Add cluster-aware tagging so that a problem text or receipt can be routed to a cluster and then to a shape. - **Pros:** Makes the survey operational inside the existing RRC/Corpus250 and AVMIsa.Emit boundary; lets the tagger reason about problem families, not just isolated equations. - **Cons:** Extending the shape taxonomy without a classifier trained on ground truth risks overfitting the survey; RRC shape decisions must stay in Lean per the programming-choice flow. - **Effort:** 3-5 days for a design pass; longer if we also update `RRC.Emit` in Lean to stamp cluster-aware receipts. ### Option D: Generate #eval witnesses / toy counterexamples for the HOLD/CANDIDATE boundaries For each problem, build a small deterministic witness that shows why its current RRC status is justified. For `HOLD` problems, demonstrate the missing axis (e.g., a proof of independence for CH). For `CANDIDATE` problems, show a concrete small-case computation (e.g., Collatz iterations up to a bounded seed). - **Pros:** Grounds the survey in executable evidence; fits the repo's `#eval` witness requirement; separates shallowly-underspecified problems from deeply-underspecified ones. - **Cons:** Toy witnesses do not prove or disprove the general statements; some `HOLD` cases (ZFC consistency, measurement problem) have principled limits. - **Effort:** 2-4 days for a first batch of 10-15 witnesses; scales linearly with the number of problems covered. ### Option E: Outreach — publish the survey as a research note or guide literature mining Publish a short research note on the survey structure, the crossing matrix, and the RRC projection methodology. Use it to solicit external reviewers and to seed `rrc_arxiv_kernel_refine.py` with targeted literature-mining queries. - **Pros:** Low engineering cost; builds reviewer provenance; may surface reduction edges the survey missed. - **Cons:** Does not directly advance the formal stack; publicity before the claim-state ladder is mature risks overclaiming. - **Effort:** 1-2 days for a note; ongoing effort to curate mined literature. --- ## Recommendation: Three-Stage Roadmap ### Stage 1 — This week: inventory and attack graph 1. Run `python3 -m py_compile` and `python3 -m json.tool` on the new survey artifacts. 2. Build a Python shim in `4-Infrastructure/shim/unsolved_problems_attack_graph.py` that reads `unsolved_hard_problems_rrc_alignments.json` and emits: - in-degree / out-degree / betweenness rankings, - reduction cascades (longest directed paths), - a list of hub problems whose solution would collapse the most leaves. 3. Validate the top 5 hub problems against the four dominant RRC shapes. 4. Save the result as `shared-data/data/stack_solidification/unsolved_problems_attack_graph_v1.json` with a receipt hash. ### Stage 2 — This month: Lean stubs and #eval witnesses 1. Create `0-Core-Formalism/lean/Semantics/Semantics/RRC/UnsolvedProblems/TopFive.lean` containing formalized statements for the top 5 hub problems. 2. Each stub records: `rrcId`, `rrcShape`, `rrcStatus`, the 10-axis vector encoded as `Q0_16` values, and a `theorem` or `def` stating the problem in Lean terms. 3. Add `#eval` witnesses that compute small finite cases (e.g., verify Collatz up to a bound, or compute prime-gap statistics) using only `Q16_16`/`Q0_16` arithmetic. 4. Update `docs/rrc_equation_classification.md` with the new `UnsolvedProblems` surface and regenerate its receipt via `AVMIsa.Emit` when the ISA rebuild permits. ### Stage 3 — This quarter: integration with Research Stack goals 1. Route the attack-graph output into `rrc_ray_tagger.py` so that each unsolved problem can be tagged with its RRC shape, cluster, and recommended ray layer. 2. Feed hub-problem receipts into the BraidStorm/eigensolid compressor as a stress-test corpus: each problem statement is a 1 KB chunk; convergence receipts measure how well the compressor captures high-semantic-entropy text. 3. Use the solved boundary marker (3D Poincare conjecture) as a positive-control receipt: its eigensolid convergence and receipt invertibility theorems should pass cleanly, providing a sanity check on the full pipeline. 4. Promote no problem beyond `CANDIDATE` in RRC space until a Lean gate explicitly passes. --- ## Open Questions / Risks - **Authority of the crossing weights.** The 30x30 matrix weights are expert-judgment estimates, not computed from citation or reduction data. Using them for centrality rankings must carry a `claim_boundary` that says "projection-only; weights are not evidence of reduction strength." - **Lean stub scope.** Stating open problems in Lean is safe if the files stay outside the main build path or use `axiom`/`sorry` with explicit `TODO(lean-port)` markers. Quarantine discipline is required. - **Shape-class overlap.** Several problems appear in multiple clusters and could plausibly map to more than one RRC shape. The pipeline must tolerate multi-shape ambiguity rather than forcing a single label. - **No Float in compute paths.** Any `#eval` witness or attack-graph score must use `Q16_16`/`Q0_16`. Raw axis scores in the JSON are already bounded in [0,1]; convert them through the fixed-point boundary, not `ofFloat`. - **Premature outreach.** Publishing before the claim-state ladder is documented could let external readers misread `CANDIDATE` as progress. Any note should repeat the projection-only boundary prominently. --- ## Required Resources / Skills | Resource | Need | |---|---| | Lean 4 / lake | Stage 2 stubs and witnesses | | Python + networkx or equivalent | Stage 1 attack graph | | RRC taxonomy knowledge | Option C and Stage 3 integration | | arXiv / literature curation | Option E and cluster refinement | | Fixed-point (Q16_16/Q0_16) discipline | All `#eval` witnesses and scoring | | Reviewer | Before any promotion beyond CANDIDATE or publication | Estimated total effort for the recommended path: **1-2 person-weeks for Stage 1**, **2-4 person-weeks for Stage 2**, and **4-8 person-weeks for Stage 3**, assuming no new dependencies and all RRC decisions remain in Lean.