01
Depend on the proof
Every product loop must use the result as a bound, obstruction, reduction, or construction—not as mathematical decoration.
~/dev/raymond$loading
I treated OpenAI’s ten formalized advances as design material: hard ceilings to score against, counterexamples that expose shortcuts, reductions that compile new challenges, and constructions that define new game worlds. All ten now have interactive vertical slices, staged by what the software can actually substantiate.
Build 01 · Proof 08 · exact geometry
Drag rational polygon vertices, hold the exact area centroid at the origin, keep every other lattice point outside the strict interior, and push the normalized score toward the proven limit of one. Guided missions, immediate recovery feedback, touch controls, and keyboard play turn the checker into a human-scale game.
The 2D release is a teaching surface and validation kernel, not a claimed mathematical discovery. The complete studio remains an owner-only prototype until public-release checks and independent rechecking are attached.
Exact score
8/9
Frontier
S(K) ≤ 1
10
interactive vertical slices
1
exact playable kernel
5
exact bounded tutorials
4
bounded research sandboxes
The portfolio rule
01
Every product loop must use the result as a bound, obstruction, reduction, or construction—not as mathematical decoration.
02
A session should produce a certificate, benchmark, construction, dataset, or decision that did not exist before.
03
Each idea names the test that would show it is only a toy, too expensive, or based on the wrong interpretation.
The ten-project atlas
Exact small cases say exact; symbolic, numerical, and provenance-first work says sandbox. Each card separates the product direction, the current implementation, and the gate required before a stronger claim.
High-dimensional sphere packing
Research game
Search for finite-dimensional auxiliary functions whose signs can be certified, not merely plotted.
Implemented now
Analytic Gaussian-mixture Fourier pairs, sampled sign-frontier plots, and explicit numerical diagnostics.
Graduation gate
Replace sampled signs with interval or algebraic continuum certificates.
Binary and spherical codes
Capacity compiler
Turn separation requirements into proof-backed feasibility envelopes for codebooks.
Implemented now
Exact finite binary codebooks, Hamming distances, sphere-packing bounds, conflict witnesses, and a deterministic greedy builder.
Graduation gate
Implement and independently verify a finite moving-subspace certificate from Chapter 2.
Non-sofic groups
Solver arena
Search for small, explicit finite-approximation obstructions inside an impossible finite-world game.
Implemented now
Exact small permutation models, word relations, normalized Hamming defects, and progressive local-law challenges.
Graduation gate
Encode theorem-specific fragments and prove a finite defect lower bound rather than observing a plateau.
Connes rigidity counterexample
Identifiability game
Test whether people and AI preserve uncertainty when different hidden systems cast the same observable shadow.
Implemented now
Exact four-state F₂² versus Z/4Z laws, factor-only controls, distinguishing probes, Bayesian updates, and proper scoring.
Graduation gate
Prove the challenge interface cannot leak a distinguishing label, then connect it to a theorem-scale symbolic fixture.
Permanent lower bounds
Circuit-complexity linter
Issue proof-backed lower-bound reports for arithmetic circuits and formulas computing the permanent.
Implemented now
Exact rational DAG evaluation, formula-versus-circuit classification, resource counts, and a six-route 3×3 permanent.
Graduation gate
Add a verified arithmetic DSL and theorem-scope reports for general symbolic permanent targets.
Quantum parallel repetition
Soundness compiler
Compile certified two-prover tests into repeated verifiers with explicit proof obligations.
Implemented now
Symbolic exp(-c ε¹³ n / (ε + ln(|A||B|))) repetition analysis, an invalid-independence comparison, and explicit alphabet and constant obligations.
Graduation gate
Attach a certified base gap and a usable traced universal constant to one end-to-end game.
Closest-vector hardness
Challenge compiler
Generate provenance-rich SAT-to-lattice benchmark bundles that can be checked end to end.
Implemented now
Strict tiny 3-CNF parsing, exhaustive SAT audits, an exact parity-lift identity, deterministic SHA-256 bundles, and JSON export.
Graduation gate
Implement the paper’s characteristic-two/Reed–Solomon front end and independently verify the full promise chain.
Ehrhart volume inequality
Exact geometry game
Grow rational convex bodies toward the sharp volume frontier while an exact checker protects every theorem condition.
Implemented now
Mission-led rational polygon editing, exact acceptance checks, recovery feedback, touch and keyboard controls, progression, and canonical certificates.
Graduation gate
Add independent certificate rechecking, equivalence deduplication, and a researcher-ready candidate atlas.
Multicolor Ramsey lower bound
Symbolic generator
Compile recursive edge-colorings into multicolor networks with no monochromatic triangles and candidate zero-error codebooks.
Implemented now
Exact complete-graph colorings, explicit monochromatic-triangle witnesses, and a verified binary-prefix K₈ seed.
Graduation gate
Materialize and independently verify a construction that beats the relevant tensor-product baseline.
Extremal graph counterexamples
Graph game and evaluation
Search for smaller or stronger examples where forbidden motifs become unexpectedly powerful together.
Implemented now
Exact small bipartite C₄/C₆ witnesses, joint-family play, and deterministic safe builders.
Graduation gate
Add independent exact optimization and theorem-specific counterexample families at meaningful sizes.
Claim boundary
These product framings are original syntheses, not certified worldwide novelty claims. A formalized theorem does not automatically validate a product, benchmark, or discovery. Every future public release still needs its own implementation evidence, independent checking, and domain-expert review.