01
Depend on the proof
Every product loop must use the result as a bound, obstruction, reduction, or construction—not as mathematical decoration.
Ten proofs. Ten product frontiers.
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
Ehrhart Frontier is the exact flagship.
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.
BigInt rational kernelexact rational checkscertificate export9 companion labs
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
The mathematics has to change the product.
02
Create an artifact
A session should produce a certificate, benchmark, construction, dataset, or decision that did not exist before.
03
Expose the falsifier
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
Ten implemented slices, staged honestly.
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.
- 01bounded research sandbox
High-dimensional sphere packing
Fourier Forge
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.
- 02exact bounded tutorial
Binary and spherical codes
Codeglass
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.
- 03bounded research sandbox
Non-sofic groups
Finite Mirage
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.
- 04exact bounded tutorial
Connes rigidity counterexample
ShadowTwin
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.
- 05exact bounded tutorial
Permanent lower bounds
PermScope
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.
- 06bounded research sandbox
Quantum parallel repetition
EntangleGuard
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.
- 07bounded research sandbox
Closest-vector hardness
GapForge
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.
- 08exact playable kernel
Ehrhart volume inequality
Ehrhart Frontier
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.
- 09exact bounded tutorial
Multicolor Ramsey lower bound
ZeroError Foundry
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.
- 10exact bounded tutorial
Extremal graph counterexamples
Motif Synergy Lab
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
Ambitious on purpose. Labeled on purpose.
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.