mirror of
https://github.com/allaunthefox/Research-Stack.git
synced 2026-07-31 03:05:21 +00:00
docs(research): path forward for RRC unsolved-problems survey
- Strategic options and 3-stage roadmap - Leverage-point analysis and top-10 ranked problems - Lean stub plan for 7 formalizable problems, 4 deferred
This commit is contained in:
parent
68db1911a4
commit
e3521925a4
3 changed files with 903 additions and 0 deletions
|
|
@ -0,0 +1,550 @@
|
|||
# Unsolved Hard Problems — Lean 4 Statement Stub Plan
|
||||
|
||||
**Date:** 2026-06-20
|
||||
**Scope:** Turn the RRC survey (`unsolved_hard_problems_rrc_survey.md` + `.json`) into precise, type-correct Lean 4 *statements* with `sorry` skeletons. No proofs are attempted.
|
||||
**Claim boundary:** This document is a build/implementation plan. It does not claim any problem is solved or that any stub will soon be provable.
|
||||
|
||||
---
|
||||
|
||||
## 1. Selection criteria
|
||||
|
||||
A problem is a **good stub target** when:
|
||||
|
||||
- Its definitions are stable in contemporary mathematics (no interpretational disputes).
|
||||
- The statement can be written with Mathlib primitives available in the pinned `v4.30.0-rc2` rev.
|
||||
- It does not depend on unsettled foundational axioms (ZFC extensions, large-cardinal hypotheses, or open-ended physical theories).
|
||||
- A finite `#eval` witness can be supplied to check small cases without floating-point arithmetic.
|
||||
|
||||
A problem is **deferred** when it is formally independent of ZFC, requires choosing an axiom system, or lacks a settled mathematical object to state.
|
||||
|
||||
---
|
||||
|
||||
## 2. Good stub targets (7 problems)
|
||||
|
||||
All modules live under `0-Core-Formalism/lean/Semantics/Semantics/Unsolved/`.
|
||||
Shared metadata lives in `Semantics.Unsolved.Metadata` and is imported by every stub.
|
||||
|
||||
### 2.1 Shared metadata module
|
||||
|
||||
**File:** `Semantics/Unsolved/Metadata.lean`
|
||||
**Namespace:** `Semantics.Unsolved.Metadata`
|
||||
|
||||
```lean
|
||||
import Semantics.FixedPoint
|
||||
|
||||
namespace Semantics.Unsolved.Metadata
|
||||
|
||||
open Semantics.FixedPoint
|
||||
|
||||
inductive RRCStatus where
|
||||
| candidate
|
||||
| hold
|
||||
| accept
|
||||
|
||||
inductive RRCShape where
|
||||
| projectableGeometryTopology
|
||||
| cognitiveLoadField
|
||||
| logogramProjection
|
||||
| burgersRgSolver
|
||||
| signalShapedRouteCompiler
|
||||
| languageSetManifoldGraph
|
||||
| holdForUnlawfulOrUnderspecifiedShape
|
||||
| computeKernelReceipt
|
||||
| cadForceProbeReceipt
|
||||
| erdosBoundConjecture
|
||||
| leanTheoremReceipt
|
||||
|
||||
structure RRCAxes where
|
||||
semanticEntropy : Q0_16
|
||||
geometricMass : Q0_16
|
||||
compressionPressure : Q0_16
|
||||
topologyTorsion : Q0_16
|
||||
residualRisk : Q0_16
|
||||
proofReadiness : Q0_16
|
||||
scaleBandDeclared : Q0_16
|
||||
negativeControlStrength : Q0_16
|
||||
projectionDeclared : Q0_16
|
||||
shapeClosure : Q0_16
|
||||
|
||||
structure ProblemMetadata where
|
||||
rrcId : String
|
||||
rrcShape : RRCShape
|
||||
rrcStatus : RRCStatus
|
||||
axes : RRCAxes
|
||||
|
||||
end Semantics.Unsolved.Metadata
|
||||
```
|
||||
|
||||
**Why it is needed:** Keeps the RRC projection data (id, shape, status, 10-axis vector) in one place and lets every problem stub carry its survey identity as a checked Lean value. Axis values are stored as `Q0_16` raw integers, not `Float`.
|
||||
|
||||
---
|
||||
|
||||
### 2.2 Goldbach conjecture
|
||||
|
||||
**File:** `Semantics/Unsolved/Goldbach.lean`
|
||||
**Namespace:** `Semantics.Unsolved.Goldbach`
|
||||
|
||||
```lean
|
||||
import Semantics.Unsolved.Metadata
|
||||
import Mathlib.Data.Nat.Prime
|
||||
import Mathlib.Data.Nat.Parity
|
||||
|
||||
namespace Semantics.Unsolved.Goldbach
|
||||
|
||||
open Semantics.Unsolved.Metadata
|
||||
|
||||
def metadata : ProblemMetadata where
|
||||
rrcId := "goldbach_conjecture"
|
||||
rrcShape := RRCShape.logogramProjection
|
||||
rrcStatus := RRCStatus.candidate
|
||||
axes := {
|
||||
semanticEntropy := Q0_16.ofRawInt 19660 -- 0.60
|
||||
geometricMass := Q0_16.ofRawInt 6553 -- 0.20
|
||||
compressionPressure := Q0_16.ofRawInt 22937 -- 0.70
|
||||
topologyTorsion := Q0_16.ofRawInt 6553 -- 0.20
|
||||
residualRisk := Q0_16.ofRawInt 9830 -- 0.30
|
||||
proofReadiness := Q0_16.ofRawInt 9830 -- 0.30
|
||||
scaleBandDeclared := Q0_16.ofRawInt 27852 -- 0.85
|
||||
negativeControlStrength := Q0_16.ofRawInt 22937 -- 0.70
|
||||
projectionDeclared := Q0_16.ofRawInt 31128 -- 0.95
|
||||
shapeClosure := Q0_16.ofRawInt 18022 -- 0.55
|
||||
}
|
||||
|
||||
def goldbach (n : Nat) : Prop :=
|
||||
n > 2 ∧ Even n → ∃ p q, p.Prime ∧ q.Prime ∧ p + q = n
|
||||
|
||||
theorem goldbachConjecture :
|
||||
∀ n, goldbach n := by
|
||||
sorry -- TODO(lean-port): no known elementary proof; verified computationally to large bounds
|
||||
|
||||
-- #eval witness: every even n in (4..10000) is a sum of two primes.
|
||||
-- Expect: true
|
||||
|
||||
end Semantics.Unsolved.Goldbach
|
||||
```
|
||||
|
||||
**Required Mathlib imports:** `Mathlib.Data.Nat.Prime`, `Mathlib.Data.Nat.Parity`.
|
||||
**Dependencies:** `Semantics.Unsolved.Metadata`.
|
||||
**Why it is a good stub target:** The statement uses only `Nat.Prime` and `Even`; both are stable. A bounded `#eval` witness is immediate.
|
||||
|
||||
---
|
||||
|
||||
### 2.3 Twin prime conjecture
|
||||
|
||||
**File:** `Semantics/Unsolved/TwinPrime.lean`
|
||||
**Namespace:** `Semantics.Unsolved.TwinPrime`
|
||||
|
||||
```lean
|
||||
import Semantics.Unsolved.Metadata
|
||||
import Mathlib.Data.Nat.Prime
|
||||
import Mathlib.Data.Set.Basic
|
||||
|
||||
namespace Semantics.Unsolved.TwinPrime
|
||||
|
||||
open Semantics.Unsolved.Metadata
|
||||
|
||||
def metadata : ProblemMetadata where
|
||||
rrcId := "twin_prime_conjecture"
|
||||
rrcShape := RRCShape.logogramProjection
|
||||
rrcStatus := RRCStatus.candidate
|
||||
axes := {
|
||||
semanticEntropy := Q0_16.ofRawInt 21300 -- 0.65
|
||||
geometricMass := Q0_16.ofRawInt 8191 -- 0.25
|
||||
compressionPressure := Q0_16.ofRawInt 24575 -- 0.75
|
||||
topologyTorsion := Q0_16.ofRawInt 8191 -- 0.25
|
||||
residualRisk := Q0_16.ofRawInt 11468 -- 0.35
|
||||
proofReadiness := Q0_16.ofRawInt 8191 -- 0.25
|
||||
scaleBandDeclared := Q0_16.ofRawInt 26213 -- 0.80
|
||||
negativeControlStrength := Q0_16.ofRawInt 21298 -- 0.65
|
||||
projectionDeclared := Q0_16.ofRawInt 29490 -- 0.90
|
||||
shapeClosure := Q0_16.ofRawInt 14745 -- 0.45
|
||||
}
|
||||
|
||||
def isTwinPrime (p : Nat) : Prop :=
|
||||
p.Prime ∧ (p + 2).Prime
|
||||
|
||||
theorem twinPrimeConjecture :
|
||||
Set.Infinite {p | isTwinPrime p} := by
|
||||
sorry -- TODO(lean-port): sieve parity obstruction; verified to large bounds
|
||||
|
||||
-- #eval witness: list twin prime pairs below 1000.
|
||||
-- Expect: a non-empty list ending with (1019, 1021) or similar
|
||||
|
||||
end Semantics.Unsolved.TwinPrime
|
||||
```
|
||||
|
||||
**Required Mathlib imports:** `Mathlib.Data.Nat.Prime`, `Mathlib.Data.Set.Basic`.
|
||||
**Dependencies:** `Semantics.Unsolved.Metadata`.
|
||||
**Why it is a good stub target:** One predicate on `Nat.Prime`; `Set.Infinite` is available. Bounded witnesses are trivial to compute.
|
||||
|
||||
---
|
||||
|
||||
### 2.4 Collatz conjecture
|
||||
|
||||
**File:** `Semantics/Unsolved/Collatz.lean`
|
||||
**Namespace:** `Semantics.Unsolved.Collatz`
|
||||
|
||||
```lean
|
||||
import Semantics.Unsolved.Metadata
|
||||
import Mathlib.Data.Nat.Basic
|
||||
|
||||
namespace Semantics.Unsolved.Collatz
|
||||
|
||||
open Semantics.Unsolved.Metadata
|
||||
|
||||
def metadata : ProblemMetadata where
|
||||
rrcId := "collatz_conjecture"
|
||||
rrcShape := RRCShape.logogramProjection
|
||||
rrcStatus := RRCStatus.candidate
|
||||
axes := {
|
||||
semanticEntropy := Q0_16.ofRawInt 18022 -- 0.55
|
||||
geometricMass := Q0_16.ofRawInt 11468 -- 0.35
|
||||
compressionPressure := Q0_16.ofRawInt 22937 -- 0.70
|
||||
topologyTorsion := Q0_16.ofRawInt 14745 -- 0.45
|
||||
residualRisk := Q0_16.ofRawInt 13107 -- 0.40
|
||||
proofReadiness := Q0_16.ofRawInt 6553 -- 0.20
|
||||
scaleBandDeclared := Q0_16.ofRawInt 26213 -- 0.80
|
||||
negativeControlStrength := Q0_16.ofRawInt 19660 -- 0.60
|
||||
projectionDeclared := Q0_16.ofRawInt 27852 -- 0.85
|
||||
shapeClosure := Q0_16.ofRawInt 13107 -- 0.40
|
||||
}
|
||||
|
||||
def collatzNext (n : Nat) : Nat :=
|
||||
if n % 2 = 0 then n / 2 else 3 * n + 1
|
||||
|
||||
def collatzSeq (n : Nat) : Nat → Nat
|
||||
| 0 => n
|
||||
| k + 1 => collatzNext (collatzSeq n k)
|
||||
|
||||
theorem collatzConjecture :
|
||||
∀ n, n > 0 → ∃ k, collatzSeq n k = 1 := by
|
||||
sorry -- TODO(lean-port): no known invariant controls expand/contract dynamics across all scales
|
||||
|
||||
-- #eval witness: verify convergence for all seeds 1..10000.
|
||||
-- Expect: true
|
||||
|
||||
end Semantics.Unsolved.Collatz
|
||||
```
|
||||
|
||||
**Required Mathlib imports:** `Mathlib.Data.Nat.Basic`.
|
||||
**Dependencies:** `Semantics.Unsolved.Metadata`.
|
||||
**Why it is a good stub target:** Pure `Nat` recursion; the statement is a single quantified property. Small-seed verification is an easy `#eval` witness.
|
||||
|
||||
---
|
||||
|
||||
### 2.5 abc conjecture
|
||||
|
||||
**File:** `Semantics/Unsolved/AbcConjecture.lean`
|
||||
**Namespace:** `Semantics.Unsolved.AbcConjecture`
|
||||
|
||||
```lean
|
||||
import Semantics.Unsolved.Metadata
|
||||
import Mathlib.Data.Nat.Prime
|
||||
import Mathlib.Data.Nat.Factorization
|
||||
import Mathlib.Data.Real.Basic
|
||||
import Mathlib.Analysis.SpecialFunctions.Pow.Real
|
||||
|
||||
namespace Semantics.Unsolved.AbcConjecture
|
||||
|
||||
open Semantics.Unsolved.Metadata
|
||||
|
||||
def metadata : ProblemMetadata where
|
||||
rrcId := "abc_conjecture"
|
||||
rrcShape := RRCShape.logogramProjection
|
||||
rrcStatus := RRCStatus.candidate
|
||||
axes := {
|
||||
semanticEntropy := Q0_16.ofRawInt 24575 -- 0.75
|
||||
geometricMass := Q0_16.ofRawInt 9830 -- 0.30
|
||||
compressionPressure := Q0_16.ofRawInt 26213 -- 0.80
|
||||
topologyTorsion := Q0_16.ofRawInt 11468 -- 0.35
|
||||
residualRisk := Q0_16.ofRawInt 13107 -- 0.40
|
||||
proofReadiness := Q0_16.ofRawInt 8191 -- 0.25
|
||||
scaleBandDeclared := Q0_16.ofRawInt 24575 -- 0.75
|
||||
negativeControlStrength := Q0_16.ofRawInt 19660 -- 0.60
|
||||
projectionDeclared := Q0_16.ofRawInt 29490 -- 0.90
|
||||
shapeClosure := Q0_16.ofRawInt 16383 -- 0.50
|
||||
}
|
||||
|
||||
/-- Radical of a positive integer: product of distinct prime divisors. -/
|
||||
def rad (n : Nat) : Nat :=
|
||||
n.factorization.prod fun p _ => p
|
||||
|
||||
theorem abcConjecture :
|
||||
∀ ε : ℝ, ε > 0 →
|
||||
∃ C : ℝ, C > 0 ∧
|
||||
∀ a b c : Nat,
|
||||
a > 0 → b > 0 → c > 0 →
|
||||
a + b = c →
|
||||
Nat.gcd a b = 1 →
|
||||
(c : ℝ) ≤ C * (rad (a * b * c) : ℝ) ^ (1 + ε : ℝ) := by
|
||||
sorry -- TODO(lean-port): deep Diophantine machinery; only partial results known
|
||||
|
||||
-- #eval witness: for ε = 0.5, check all coprime triples a + b = c ≤ 100.
|
||||
-- Expect: no counterexample found
|
||||
|
||||
end Semantics.Unsolved.AbcConjecture
|
||||
```
|
||||
|
||||
**Required Mathlib imports:** `Mathlib.Data.Nat.Prime`, `Mathlib.Data.Nat.Factorization`, `Mathlib.Data.Real.Basic`, `Mathlib.Analysis.SpecialFunctions.Pow.Real`.
|
||||
**Dependencies:** `Semantics.Unsolved.Metadata`.
|
||||
**Why it is a good stub target:** `Nat.factorization` and real exponentiation are present in the pinned mathlib. The statement is a single inequality with explicit quantifiers.
|
||||
|
||||
---
|
||||
|
||||
### 2.6 Beal conjecture
|
||||
|
||||
**File:** `Semantics/Unsolved/BealConjecture.lean`
|
||||
**Namespace:** `Semantics.Unsolved.BealConjecture`
|
||||
|
||||
```lean
|
||||
import Semantics.Unsolved.Metadata
|
||||
import Mathlib.Data.Nat.Prime
|
||||
|
||||
namespace Semantics.Unsolved.BealConjecture
|
||||
|
||||
open Semantics.Unsolved.Metadata
|
||||
|
||||
def metadata : ProblemMetadata where
|
||||
rrcId := "beal_conjecture"
|
||||
rrcShape := RRCShape.logogramProjection
|
||||
rrcStatus := RRCStatus.candidate
|
||||
axes := {
|
||||
semanticEntropy := Q0_16.ofRawInt 21298 -- 0.65
|
||||
geometricMass := Q0_16.ofRawInt 8191 -- 0.25
|
||||
compressionPressure := Q0_16.ofRawInt 22937 -- 0.70
|
||||
topologyTorsion := Q0_16.ofRawInt 8191 -- 0.25
|
||||
residualRisk := Q0_16.ofRawInt 9830 -- 0.30
|
||||
proofReadiness := Q0_16.ofRawInt 6553 -- 0.20
|
||||
scaleBandDeclared := Q0_16.ofRawInt 24575 -- 0.75
|
||||
negativeControlStrength := Q0_16.ofRawInt 18022 -- 0.55
|
||||
projectionDeclared := Q0_16.ofRawInt 27852 -- 0.85
|
||||
shapeClosure := Q0_16.ofRawInt 13107 -- 0.40
|
||||
}
|
||||
|
||||
def commonPrimeFactor (a b c : Nat) : Prop :=
|
||||
∃ p, p.Prime ∧ p ∣ a ∧ p ∣ b ∧ p ∣ c
|
||||
|
||||
theorem bealConjecture :
|
||||
∀ a b c x y z : Nat,
|
||||
a > 0 → b > 0 → c > 0 →
|
||||
x > 2 → y > 2 → z > 2 →
|
||||
a ^ x + b ^ y = c ^ z →
|
||||
commonPrimeFactor a b c := by
|
||||
sorry -- TODO(lean-port): would follow from abc; special cases and parametric families known
|
||||
|
||||
-- #eval witness: check all a^x + b^y = c^z with bases ≤ 20 and exponents ≤ 5.
|
||||
-- Expect: every solution has a common prime factor
|
||||
|
||||
end Semantics.Unsolved.BealConjecture
|
||||
```
|
||||
|
||||
**Required Mathlib imports:** `Mathlib.Data.Nat.Prime`.
|
||||
**Dependencies:** `Semantics.Unsolved.Metadata`.
|
||||
**Why it is a good stub target:** Purely about `Nat.Prime` and divisibility. The statement is a simple Diophantine implication.
|
||||
|
||||
---
|
||||
|
||||
### 2.7 Brocard's problem
|
||||
|
||||
**File:** `Semantics/Unsolved/Brocard.lean`
|
||||
**Namespace:** `Semantics.Unsolved.Brocard`
|
||||
|
||||
```lean
|
||||
import Semantics.Unsolved.Metadata
|
||||
import Mathlib.Data.Nat.Basic
|
||||
|
||||
namespace Semantics.Unsolved.Brocard
|
||||
|
||||
open Semantics.Unsolved.Metadata
|
||||
|
||||
def metadata : ProblemMetadata where
|
||||
rrcId := "brocards_problem"
|
||||
rrcShape := RRCShape.logogramProjection
|
||||
rrcStatus := RRCStatus.candidate
|
||||
axes := {
|
||||
semanticEntropy := Q0_16.ofRawInt 18022 -- 0.55
|
||||
geometricMass := Q0_16.ofRawInt 6553 -- 0.20
|
||||
compressionPressure := Q0_16.ofRawInt 19660 -- 0.60
|
||||
topologyTorsion := Q0_16.ofRawInt 6553 -- 0.20
|
||||
residualRisk := Q0_16.ofRawInt 11468 -- 0.35
|
||||
proofReadiness := Q0_16.ofRawInt 6553 -- 0.20
|
||||
scaleBandDeclared := Q0_16.ofRawInt 22937 -- 0.70
|
||||
negativeControlStrength := Q0_16.ofRawInt 18022 -- 0.55
|
||||
projectionDeclared := Q0_16.ofRawInt 27852 -- 0.85
|
||||
shapeClosure := Q0_16.ofRawInt 16383 -- 0.50
|
||||
}
|
||||
|
||||
def isBrocardSolution (n m : Nat) : Prop :=
|
||||
n.factorial + 1 = m ^ 2
|
||||
|
||||
theorem brocardProblem :
|
||||
{n | ∃ m, isBrocardSolution n m} = {4, 5, 7} := by
|
||||
sorry -- TODO(lean-port): expected finite list; only n = 4, 5, 7 are known
|
||||
|
||||
-- #eval witness: verify 4!+1 = 5², 5!+1 = 11², 7!+1 = 71².
|
||||
-- Expect: true
|
||||
|
||||
end Semantics.Unsolved.Brocard
|
||||
```
|
||||
|
||||
**Required Mathlib imports:** `Mathlib.Data.Nat.Basic`.
|
||||
**Dependencies:** `Semantics.Unsolved.Metadata`.
|
||||
**Why it is a good stub target:** Uses only `Nat.factorial` and square equality. The conjectured answer is a finite set, making the statement concrete.
|
||||
|
||||
---
|
||||
|
||||
### 2.8 Odd perfect numbers
|
||||
|
||||
**File:** `Semantics/Unsolved/OddPerfect.lean`
|
||||
**Namespace:** `Semantics.Unsolved.OddPerfect`
|
||||
|
||||
```lean
|
||||
import Semantics.Unsolved.Metadata
|
||||
import Mathlib.Data.Nat.Basic
|
||||
import Mathlib.Data.Nat.Parity
|
||||
|
||||
namespace Semantics.Unsolved.OddPerfect
|
||||
|
||||
open Semantics.Unsolved.Metadata
|
||||
|
||||
def metadata : ProblemMetadata where
|
||||
rrcId := "perfect_numbers_odd_existence"
|
||||
rrcShape := RRCShape.logogramProjection
|
||||
rrcStatus := RRCStatus.candidate
|
||||
axes := {
|
||||
semanticEntropy := Q0_16.ofRawInt 19660 -- 0.60
|
||||
geometricMass := Q0_16.ofRawInt 6553 -- 0.20
|
||||
compressionPressure := Q0_16.ofRawInt 21298 -- 0.65
|
||||
topologyTorsion := Q0_16.ofRawInt 6553 -- 0.20
|
||||
residualRisk := Q0_16.ofRawInt 11468 -- 0.35
|
||||
proofReadiness := Q0_16.ofRawInt 6553 -- 0.20
|
||||
scaleBandDeclared := Q0_16.ofRawInt 26213 -- 0.80
|
||||
negativeControlStrength := Q0_16.ofRawInt 19660 -- 0.60
|
||||
projectionDeclared := Q0_16.ofRawInt 27852 -- 0.85
|
||||
shapeClosure := Q0_16.ofRawInt 16383 -- 0.50
|
||||
}
|
||||
|
||||
/-- n is perfect iff the sum of its proper divisors equals n. -/
|
||||
def isPerfect (n : Nat) : Prop :=
|
||||
n.divisors.sum id = 2 * n
|
||||
|
||||
theorem noOddPerfectNumbers :
|
||||
¬∃ n, Odd n ∧ n > 0 ∧ isPerfect n := by
|
||||
sorry -- TODO(lean-port): no example or impossibility proof known; many restrictions proven
|
||||
|
||||
-- #eval witness: no odd perfect number below 10^5.
|
||||
-- Expect: true
|
||||
|
||||
end Semantics.Unsolved.OddPerfect
|
||||
```
|
||||
|
||||
**Required Mathlib imports:** `Mathlib.Data.Nat.Basic`, `Mathlib.Data.Nat.Parity`.
|
||||
**Dependencies:** `Semantics.Unsolved.Metadata`.
|
||||
**Why it is a good stub target:** `Nat.divisors.sum` is available; the statement is an existence/impossibility claim with a clean negation.
|
||||
|
||||
---
|
||||
|
||||
## 3. Deferred poor stub targets (4 problems)
|
||||
|
||||
These problems are intentionally excluded from the first stub pass.
|
||||
|
||||
### 3.1 Continuum Hypothesis
|
||||
|
||||
**Survey id:** `continuum_hypothesis`
|
||||
**Why deferred:** Independent of ZFC by Gödel and Cohen. A Lean formalization would require either (a) adopting a specific set-theoretic universe/forcing extension, which is not a settled definition, or (b) proving `ZFC ⊢ CH` or `ZFC ⊢ ¬CH`, both impossible. Stating it as a bare `Prop` gives no useful formal surface.
|
||||
|
||||
### 3.2 Consistency of ZFC
|
||||
|
||||
**Survey id:** `consistency_of_zfc`
|
||||
**Why deferred:** Gödel's second incompleteness theorem shows ZFC cannot prove its own consistency unless inconsistent. Any formal statement would have to be conditional on a stronger metatheory, violating the "stable definitions" criterion.
|
||||
|
||||
### 3.3 Hilbert's 6th problem
|
||||
|
||||
**Survey id:** `hilbert_sixth_problem`
|
||||
**Why deferred:** The problem asks to "axiomatize all of physics." Physics is a collection of effective theories; there is no single agreed-upon object to formalize. The statement is open-ended rather than a well-posed mathematical proposition.
|
||||
|
||||
### 3.4 Quantum measurement problem
|
||||
|
||||
**Survey id:** `measurement_problem`
|
||||
**Why deferred:** It is interpretational. Different solutions (Copenhagen, many-worlds, Bohmian, decoherence-only, etc.) define the measurement process differently. A formal statement would embed an unresolved interpretational choice.
|
||||
|
||||
---
|
||||
|
||||
## 4. Build strategy
|
||||
|
||||
### 4.1 Quarantine the stubs from the default build
|
||||
|
||||
Add a dedicated `Unsolved` lean library in `lakefile.toml` and keep it out of `defaultTargets`:
|
||||
|
||||
```toml
|
||||
[[lean_lib]]
|
||||
name = "Unsolved"
|
||||
roots = ["Semantics.Unsolved"]
|
||||
```
|
||||
|
||||
Do **not** add `Unsolved` to `defaultTargets`.
|
||||
The default `lake build` (which builds `Compiler` + `Semantics`) therefore stays green.
|
||||
Developers check stubs with:
|
||||
|
||||
```bash
|
||||
lake build Semantics.Unsolved.Goldbach
|
||||
lake build Unsolved
|
||||
```
|
||||
|
||||
If the existing `Semantics` lean_lib auto-discovers the same `Semantics.Unsolved.*` modules, narrow `Semantics.roots` during stub development so that `Semantics` no longer traverses `Semantics.Unsolved`.
|
||||
|
||||
### 4.2 `sorry` discipline
|
||||
|
||||
Every theorem skeleton uses `sorry` with a `TODO(lean-port)` comment that explains the obstruction, per the `lean-proof` skill contract. Example:
|
||||
|
||||
```lean
|
||||
theorem goldbachConjecture : ∀ n, goldbach n := by
|
||||
sorry -- TODO(lean-port): no known elementary proof; verified computationally to large bounds
|
||||
```
|
||||
|
||||
No bare `sorry` is allowed.
|
||||
|
||||
### 4.3 `#eval` witnesses
|
||||
|
||||
Each stub includes at least one `#eval` witness for a finite, computable special case:
|
||||
|
||||
| Problem | Witness |
|
||||
|---------|---------|
|
||||
| Goldbach | Verify the conjecture for all even `n ≤ 10000`. |
|
||||
| Twin prime | Enumerate twin prime pairs below 1000. |
|
||||
| Collatz | Verify convergence for all seeds `1..10000`. |
|
||||
| abc | For `ε = 0.5`, scan coprime triples `a + b = c ≤ 100`. |
|
||||
| Beal | Scan `a^x + b^y = c^z` with small bases/exponents. |
|
||||
| Brocard | Confirm `4!+1 = 5²`, `5!+1 = 11²`, `7!+1 = 71²`. |
|
||||
| Odd perfect | Confirm no odd perfect number below `10^5`. |
|
||||
|
||||
All witnesses use `Nat`/`Int` computation or `Q0_16` axis encoding. No `Float` appears in any compute path.
|
||||
|
||||
### 4.4 Start order
|
||||
|
||||
1. **First:** `Semantics.Unsolved.Metadata` — defines the shared RRC vocabulary and proves it has no `sorry`.
|
||||
2. **Second:** `Semantics.Unsolved.Goldbach` and `Semantics.Unsolved.TwinPrime` — simplest definitions, used to validate the build/quarantine setup.
|
||||
3. **Third:** `Semantics.Unsolved.Collatz` — tests a well-founded recursive definition in the stub namespace.
|
||||
4. **Fourth:** `Semantics.Unsolved.AbcConjecture`, `Semantics.Unsolved.BealConjecture`, `Semantics.Unsolved.Brocard`, `Semantics.Unsolved.OddPerfect` — number-theory stubs that import prime/divisor/factorial machinery.
|
||||
|
||||
### 4.5 Promotion rule
|
||||
|
||||
A stub may be promoted into the main `Semantics` library only when its theorem is either fully proved or replaced by an explicit `axiom` that names the model boundary (e.g., `axiom goldbachConjecture`). Until then, `Unsolved` stays quarantined.
|
||||
|
||||
---
|
||||
|
||||
## 5. Research Stack conventions
|
||||
|
||||
- **Fixed-point only:** RRC axis scores are encoded as `Q0_16` raw integers via `Q0_16.ofRawInt`. No `Float` is used in compute paths.
|
||||
- **Receipt boundary:** The `Unsolved` modules must not emit top-level JSON receipts. If a corpus-wide receipt for the stub collection is ever needed, it must be produced through `Semantics.AVMIsa.Emit`, which is the sole output boundary.
|
||||
- **No new dependencies:** All definitions rely on the existing mathlib pin (`v4.30.0-rc2`) and the repo's `Semantics.FixedPoint` module.
|
||||
- **Naming:** Files and namespaces use `PascalCase` per `LEAN_NAMING_CONVENTIONS.md`.
|
||||
- **No broad staging:** When the stubs are eventually committed, stage only the planned `Unsolved/` files plus `lakefile.toml` changes. Do not use `git add .`.
|
||||
|
||||
---
|
||||
|
||||
## 6. Open questions
|
||||
|
||||
- Should the `Unsolved` library eventually be wired into `RRC.Emit` as a read-only corpus, or kept as a separate formalization target?
|
||||
- Should the finite `#eval` witnesses be extracted into a single `Unsolved/Witnesses.lean` module to avoid re-running expensive checks during every stub build?
|
||||
- Should the survey's 30x30 reduction matrix be formalized as a `Finset`-based relation between `ProblemMetadata.rrcId` values before the stubs are expanded beyond these seven?
|
||||
|
|
@ -0,0 +1,237 @@
|
|||
# RRC Unsolved-Problems Leverage Analysis
|
||||
|
||||
**Source:** `6-Documentation/docs/research/unsolved_hard_problems_rrc_alignments.json`
|
||||
**Schema:** `unsolved_hard_problems_rrc_alignments_v1` (68 problems, 67 unsolved, 1 solved boundary)
|
||||
**Generated:** 2026-06-20
|
||||
|
||||
## 1. Methodology
|
||||
|
||||
I modeled the artifact as a directed influence graph:
|
||||
|
||||
- **Nodes:** the 67 unsolved problems (the solved 3D Poincaré boundary marker was excluded).
|
||||
- **Edge weights** were assembled from two sources:
|
||||
1. The `crossing_matrix` row for each problem (0–1 connection strengths).
|
||||
2. `known_reductions_to` / `known_reductions_from` lists: a known reduction between *A* and *B* adds a 0.25 machinery bonus to the corresponding directed edge, because solving the stronger statement typically collapses or heavily informs the weaker one.
|
||||
- **Direction:** an edge `X → Y` means "solving X is expected to unlock or collapse Y" via reduction, shared machinery, or analogy.
|
||||
|
||||
### Leverage scoring
|
||||
|
||||
For each problem I computed four normalized components and combined them into a composite leverage score:
|
||||
|
||||
| Component | Weight | Meaning |
|
||||
|-----------|--------|---------|
|
||||
| Strong weighted out-degree (edges ≥ 0.5) | 30 % | Direct, high-confidence unlock pressure |
|
||||
| Strong transitive reach (edges ≥ 0.5) | 25 % | Number of problems reachable through rigorous-looking reductions / machinery |
|
||||
| Two-hop strong reach | 20 % | Immediate cascade depth before saturation |
|
||||
| Cross-cluster bridging (strong edges) | 15 % | Number of distinct alignment clusters unlocked outside the node's home cluster |
|
||||
| Strong degree count | 10 % | Count of direct high-confidence outgoing edges |
|
||||
|
||||
I also ran a second pass with a 0.3 threshold to capture shared-technique / analogical links. The results below distinguish the two whenever the difference matters.
|
||||
|
||||
## 2. Ranked Top-10 Leverage Problems
|
||||
|
||||
The scoring is dominated by the computational-complexity core: P vs NP and its satellites act as the artifact's central routing hub. Only one non-complexity problem (Birch–Swinnerton-Dyer) cracks the extended top 15.
|
||||
|
||||
| Rank | Problem | ID | Composite score | Strong reach | Cross clusters (strong) | RRC shape | RRC status | Home cluster |
|
||||
|------|---------|----|-----------------|--------------|------------------------|-----------|------------|--------------|
|
||||
| 1 | **P vs NP** | `p_vs_np` | 0.975 | 11 | 2 | `CognitiveLoadField` | CANDIDATE | cluster_02 (Complexity) |
|
||||
| 2 | **Unique Games Conjecture** | `unique_games_conjecture` | 0.900 | 11 | 2 | `CognitiveLoadField` | CANDIDATE | cluster_02 |
|
||||
| 3 | **Exponential Time Hypothesis** | `exponential_time_hypothesis` | 0.890 | 11 | 2 | `CognitiveLoadField` | CANDIDATE | cluster_02 |
|
||||
| 4 | **BPP vs P (derandomization)** | `bpp_vs_p` | 0.885 | 11 | 2 | `CognitiveLoadField` | HOLD | cluster_02 |
|
||||
| 5 | **Strong Exponential Time Hypothesis** | `strong_exponential_time_hypothesis` | 0.871 | 11 | 2 | `CognitiveLoadField` | CANDIDATE | cluster_02 |
|
||||
| 6 | **Discrete logarithm in P** | `discrete_log_in_p` | 0.867 | 11 | 2 | `CognitiveLoadField` | CANDIDATE | cluster_02 |
|
||||
| 7 | **Existence of NP-intermediate problems** | `np_intermediate_existence` | 0.846 | 11 | 2 | `CognitiveLoadField` | HOLD | cluster_02 |
|
||||
| 8 | **Integer factorization in P** | `factoring_in_p` | 0.829 | 11 | 2 | `CognitiveLoadField` | CANDIDATE | cluster_02 |
|
||||
| 9 | **Graph isomorphism in P?** | `graph_isomorphism_in_p` | 0.808 | 11 | 2 | `CognitiveLoadField` | CANDIDATE | cluster_02 |
|
||||
| 10 | **Quantum supremacy verification** | `quantum_supremacy_verification` | 0.617 | 11 | 2 | `ComputeKernelReceipt` | HOLD | cluster_07 (Quantum/information) |
|
||||
|
||||
### Details per top problem
|
||||
|
||||
1. **P vs NP** (`p_vs_np`)
|
||||
- **Home cluster:** `cluster_02` (Computational complexity core); the artifact also lists it in `cluster_06` (Logic/foundations).
|
||||
- **Clusters connected (strong):** cluster_02, cluster_03 (PDE/field singularities), cluster_07 (quantum/information).
|
||||
- **Direct strong unlocks:** BPP vs P, discrete log, ETH, factoring, graph isomorphism, NP-intermediate existence, quantum supremacy verification, SETH, UGC.
|
||||
- **With analogies (≥0.3):** also reaches continuum hypothesis, consistency of ZFC, cosmological constant, dark matter, Navier–Stokes, Hilbert's 6th/16th, Yang–Mills mass gap (via quantum supremacy).
|
||||
- **Why it tops the list:** highest strong weighted out-degree (7.20) and the broadest set of direct strong edges in the artifact.
|
||||
|
||||
2. **Unique Games Conjecture** (`unique_games_conjecture`)
|
||||
- **Home cluster:** `cluster_02`.
|
||||
- **Clusters connected (strong):** cluster_02, cluster_03, cluster_07.
|
||||
- **Direct strong unlocks:** BPP vs P, discrete log, ETH, factoring, graph isomorphism, NP-intermediate, P vs NP, small-set expansion, SETH.
|
||||
- **Note:** UGC and small-set expansion are mutually reducible in the artifact; UGC is the more central hub.
|
||||
|
||||
3. **Exponential Time Hypothesis** (`exponential_time_hypothesis`)
|
||||
- **Home cluster:** `cluster_02`.
|
||||
- **Clusters connected (strong):** cluster_02, cluster_03, cluster_07.
|
||||
- **Direct strong unlocks:** BPP vs P, discrete log, factoring, graph isomorphism, NP-intermediate, P vs NP, SETH, UGC.
|
||||
- **Role:** fine-grained-complexity anchor; its collapse propagates through the entire complexity web.
|
||||
|
||||
4. **BPP vs P (derandomization)** (`bpp_vs_p`)
|
||||
- **Home cluster:** `cluster_02`.
|
||||
- **Clusters connected (strong):** cluster_02, cluster_03, cluster_07.
|
||||
- **Direct strong unlocks:** discrete log, ETH, factoring, graph isomorphism, NP-intermediate existence, P vs NP, quantum supremacy, SETH, UGC.
|
||||
- **Status:** HOLD (the artifact flags derandomization as currently blocked by circuit-lower-bound barriers).
|
||||
|
||||
5. **Strong Exponential Time Hypothesis** (`strong_exponential_time_hypothesis`)
|
||||
- **Home cluster:** `cluster_02`.
|
||||
- **Clusters connected (strong):** cluster_02, cluster_03, cluster_07.
|
||||
- **Direct strong unlocks:** BPP vs P, discrete log, ETH, factoring, graph isomorphism, NP-intermediate, P vs NP, UGC.
|
||||
- **Relationship:** tightly coupled to ETH (1.30 mutual edge), so solving either collapses the other and the rest of the cluster.
|
||||
|
||||
6. **Discrete logarithm in P** (`discrete_log_in_p`)
|
||||
- **Home cluster:** `cluster_02`.
|
||||
- **Clusters connected (strong):** cluster_02, cluster_03, cluster_07.
|
||||
- **Direct strong unlocks:** BPP vs P, ETH, factoring, graph isomorphism, NP-intermediate, P vs NP, SETH, UGC.
|
||||
- **Note:** mutually reducible with factoring; together they are the cryptographic hardness sub-hub.
|
||||
|
||||
7. **Existence of NP-intermediate problems** (`np_intermediate_existence`)
|
||||
- **Home cluster:** `cluster_02`.
|
||||
- **Clusters connected (strong):** cluster_02, cluster_03, cluster_07.
|
||||
- **Direct strong unlocks:** BPP vs P, discrete log, ETH, factoring, graph isomorphism, P vs NP, SETH, UGC.
|
||||
- **Status:** HOLD — the artifact notes it is conditional on P ≠ NP, so it is essentially a corollary-shaped gate.
|
||||
|
||||
8. **Integer factorization in P** (`factoring_in_p`)
|
||||
- **Home cluster:** `cluster_02`.
|
||||
- **Clusters connected (strong):** cluster_02, cluster_03, cluster_07.
|
||||
- **Direct strong unlocks:** BPP vs P, discrete log, ETH, NP-intermediate, P vs NP, SETH, UGC.
|
||||
- **Note:** like discrete log, a concrete algorithmic collapse node rather than a purely logical implication.
|
||||
|
||||
9. **Graph isomorphism in P?** (`graph_isomorphism_in_p`)
|
||||
- **Home cluster:** `cluster_02`.
|
||||
- **Clusters connected (strong):** cluster_02, cluster_03, cluster_07.
|
||||
- **Direct strong unlocks:** BPP vs P, discrete log, ETH, NP-intermediate, P vs NP, SETH, UGC.
|
||||
- **Distinctive feature:** its quasipolynomial witness gives it the highest `proof_readiness` (0.30) among the top complexity nodes.
|
||||
|
||||
10. **Quantum supremacy verification** (`quantum_supremacy_verification`)
|
||||
- **Home cluster:** `cluster_07` (Quantum and information).
|
||||
- **Clusters connected (strong):** cluster_02, cluster_03.
|
||||
- **Direct strong unlocks:** P vs NP, Yang–Mills mass gap.
|
||||
- **Why it ranks here despite fewer direct edges:** it sits in `cluster_07` and has high cross-cluster bridging; from it the strong transitive closure reaches the full complexity core and PDE/field-singularity nodes.
|
||||
- **Status:** HOLD — the artifact treats the verification gap as underspecified.
|
||||
|
||||
## 3. Cluster-Specific Leverage Leaders
|
||||
|
||||
Because the global top 10 is almost entirely the complexity core, the non-complexity clusters each have their own local leverage nodes. These are the best "entry points" if the goal is to collapse a particular domain rather than the whole graph.
|
||||
|
||||
| Cluster | Best leverage node | Score | Strong reach | Key unlocks |
|
||||
|---------|-------------------|-------|--------------|-------------|
|
||||
| cluster_01 — Millennium, L-functions, motives | **Riemann Hypothesis** | 0.289 | 4 | GRH, Birch–Swinnerton-Dyer, Hodge, twin primes |
|
||||
| cluster_03 — PDE regularity/singularities | **Hilbert's 16th problem** | 0.165 | 2 | Navier–Stokes existence, Yang–Mills mass gap |
|
||||
| cluster_04 — Arithmetic/Diophantine | **Twin prime conjecture** | 0.312 | 4 | Polignac, Elliott–Halberstam, Schinzel H, Goldbach |
|
||||
| cluster_05 — Topology/geometry | **Smooth 4D Poincaré conjecture** | 0.090 | 1 | Generalized Poincaré (smooth) |
|
||||
| cluster_08 — Cosmology/dark sectors | **Dark energy equation of state** | 0.199 | 3 | Cosmological constant, dark matter, inflation |
|
||||
| cluster_09 — Fluid/field singularities | **Navier–Stokes existence and smoothness** | 0.197 | 2 | Navier–Stokes blow-up, Yang–Mills mass gap |
|
||||
| cluster_10 — Algebraic geometry/motives | **Birch and Swinnerton-Dyer conjecture** | 0.499 | 8 | Hodge, Tate, standard conjectures, rational points, Langlands |
|
||||
| unclustered | **Quantum measurement problem** | 0.210 | 2 | Quantum gravity, Hilbert's 6th problem |
|
||||
|
||||
## 4. Minimum Collapsing Subset
|
||||
|
||||
A greedy set-cover over the strong-edge (≥0.5) transitive reach selects **14 problems** that together cover all 67 unsolved problems in the artifact:
|
||||
|
||||
1. Algebrization barrier (`p_np_algebrization_barrier`)
|
||||
2. Birch and Swinnerton-Dyer conjecture
|
||||
3. Dark energy equation of state
|
||||
4. Quantum measurement problem
|
||||
5. Navier–Stokes existence and smoothness
|
||||
6. abc conjecture
|
||||
7. Singular Cardinal Hypothesis
|
||||
8. Hilbert's 16th problem
|
||||
9. Beal conjecture
|
||||
10. Smooth 4D Poincaré conjecture
|
||||
11. Generalized Poincaré conjecture (smooth category)
|
||||
12. Borel conjecture
|
||||
13. Cap set problem (exact growth)
|
||||
14. Langlands program
|
||||
|
||||
If analogical / shared-technique links (≥0.3) are included, the greedy cover collapses to **4 problems**: algebrization barrier, Schinzel's Hypothesis H, Borel conjecture, and cap set problem. This dramatic shrinkage shows how much of the artifact's connectivity is carried by cross-domain analogy rather than formal reduction.
|
||||
|
||||
## 5. Network Diagram
|
||||
|
||||
The diagram below shows the top leverage nodes and their strongest edges (weight ≥ 0.5). Thickness is omitted; all shown edges are high-confidence machinery/reduction links. Analogical weaker edges are suppressed to keep the diagram readable.
|
||||
|
||||
```mermaid
|
||||
graph LR
|
||||
subgraph ComplexityCore [cluster_02 — Complexity core]
|
||||
PNP[p_vs_np]
|
||||
UGC[unique_games_conjecture]
|
||||
ETH[exponential_time_hypothesis]
|
||||
SETH[strong_exponential_time_hypothesis]
|
||||
BPP[bpp_vs_p]
|
||||
DLOG[discrete_log_in_p]
|
||||
FACT[factoring_in_p]
|
||||
GI[graph_isomorphism_in_p]
|
||||
NPI[np_intermediate_existence]
|
||||
end
|
||||
|
||||
subgraph QuantumInfo [cluster_07 — Quantum & information]
|
||||
QS[quantum_supremacy_verification]
|
||||
YM[yang_mills_mass_gap]
|
||||
end
|
||||
|
||||
subgraph PDE [cluster_09 — Fluid/field singularities]
|
||||
NS[navier_stokes_existence_smoothness]
|
||||
H16[hilbert_sixteenth_problem]
|
||||
end
|
||||
|
||||
subgraph Foundations [cluster_06 — Logic/foundations]
|
||||
ALG[p_np_algebrization_barrier]
|
||||
end
|
||||
|
||||
subgraph Arithmetic [cluster_04 — Arithmetic/Diophantine]
|
||||
TP[twin_prime_conjecture]
|
||||
end
|
||||
|
||||
subgraph Motives [cluster_01/10 — L-functions & motives]
|
||||
RH[riemann_hypothesis]
|
||||
BSD[birch_swinnerton_dyer_conjecture]
|
||||
HODGE[hodge_conjecture]
|
||||
TATE[tate_conjecture]
|
||||
end
|
||||
|
||||
PNP --> BPP
|
||||
PNP --> DLOG
|
||||
PNP --> ETH
|
||||
PNP --> FACT
|
||||
PNP --> GI
|
||||
PNP --> NPI
|
||||
PNP --> QS
|
||||
PNP --> SETH
|
||||
PNP --> UGC
|
||||
|
||||
UGC --> PNP
|
||||
UGC --> ETH
|
||||
UGC --> SETH
|
||||
|
||||
ETH --> SETH
|
||||
SETH --> ETH
|
||||
|
||||
DLOG --> FACT
|
||||
FACT --> DLOG
|
||||
|
||||
QS --> PNP
|
||||
QS --> YM
|
||||
|
||||
YM --> H16
|
||||
NS --> H16
|
||||
H16 --> NS
|
||||
H16 --> YM
|
||||
|
||||
ALG --> PNP
|
||||
|
||||
RH --> TP
|
||||
TP --> RH
|
||||
|
||||
BSD --> RH
|
||||
BSD --> HODGE
|
||||
BSD --> TATE
|
||||
HODGE --> TATE
|
||||
TATE --> HODGE
|
||||
```
|
||||
|
||||
## 6. Caveats
|
||||
|
||||
- **Analogy vs. rigorous reduction.** Many cross-cluster edges in the artifact are 0.3–0.4 and are annotated as "shared techniques, cluster co-membership, and analogies." The strong-edge (≥0.5) analysis filters these out, but even the 0.5 threshold is a heuristic. Solving P vs NP will not automatically prove the cosmological constant problem or Hilbert's 6th problem; the artifact encodes a belief that progress on the complexity boundary propagates as *methodology*, not as formal implication.
|
||||
- **Cluster-internal vs. cross-cluster impact.** The top global nodes are high-impact inside the complexity cluster and modestly bridge into quantum/PDE/foundations. Within arithmetic, the Riemann Hypothesis / abc / twin-prime triangle is far more levered than P vs NP, even though the global score is lower.
|
||||
- **Directionality.** Edges represent "solving X unlocks Y," but reductions are not always one-way. Some pairs (P vs NP ↔ UGC, ETH ↔ SETH, factoring ↔ discrete log, abc ↔ Beal) are mutually linked, so either endpoint would collapse the other.
|
||||
- **Status bias.** Several top-scoring nodes (`bpp_vs_p`, `np_intermediate_existence`, `quantum_supremacy_verification`, `p_np_algebrization_barrier`) are in `HOLD` status, meaning the artifact already considers them underspecified or blocked. High leverage does not imply high tractability.
|
||||
- **Coverage is not collapse.** The set-cover result shows that 14 (or 4, with analogy) nodes *touch* every other problem in the graph. It does not mean proving those 14 would prove all 67; it means every other problem has at least one analogical or reduction path back to one of them.
|
||||
|
|
@ -0,0 +1,116 @@
|
|||
# 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.
|
||||
Loading…
Add table
Reference in a new issue