Open Problems Lab — Intake Archive

Question

Can a Lean-centered lab admit open-problem proposals without letting prompts, surveys, or partial certificates impersonate proofs?

Context

Open Problems Lab is Club B verify infrastructure for the Recursive Self Improvement Lab: mathematical open problems enter through bounded certificates and a kernel-checked gate. Prompts may propose; only Lean acceptance promotes. The first public result is deliberately an intake archive — healthy source structure, explicit hashes, and zero promoted proofs — so the lab cannot confuse activity with progress.

flowchart TB
  intake["Problem record + prompts"]
  registry["Typed registries + hashes"]
  lean["Lean fixtures + forbidden-token checks"]
  mathlib["Mathlib / lake CI"]
  promote["Kernel-checked promotion"]

  intake --> registry --> lean --> mathlib -->|"blocked today"| promote
  lean -->|"adversarial fixtures"| lean

Findings

• Intake archive holds 15 problem records, 29 prompt rows, and a matching 15-row survey.
• Audit found two redacted full-problem targets and no solutions, verifier code, test cases, split metadata, or per-problem citations in the public intake surface.
• Deterministic intake layer emits typed registries for all 15 problems and 29 prompt variants and passes seven validation tests.
• Lean 4.32.0 layer carries immutable target hashes, strict import and forbidden-token checks, and five passing adversarial fixture tests.
• Kernel acceptance is blocked: Mathlib commit is checked out, but dependency resolution timed out before lake-manifest.json, so the Lean CI gate has not run. Zero proofs promoted.
• Lorenz’s paused RLM harness contributed the proof-integrity patterns reused here; Open Problems Lab is the narrower, source-grounded continuation.

Method

Verifier-first discipline reused from sibling labs (proof-integrity and proposal-ranking patterns) without accepting dirty worktrees wholesale. Archive hashes and Lean fixtures are the sealed boundary; computational certificates and search remain gated behind kernel CI. A prompt that looks like a proof is still only a prompt until the kernel accepts it.

Limits

• Mathlib dependency resolution timed out before the full Lean CI gate could run.
• The public archive contains prompts and target records, not solutions.
• Two full-problem targets are redacted in the public surface.
• Intake health is not evidence that any open problem has been solved.

Artifact

Executable truth lives in the private open-problems-lab repository. This report is the public intake status; a notebook export will follow once the Mathlib gate is green and a first benchmark contract is frozen.