Research-Stack/6-Documentation/docs/research/unsolved_hard_problems_lean_stubs_plan.md

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

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

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

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

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

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

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

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

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:

[[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:

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:

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?