Publish static OProver results lab

README.md

@@ -1,10 +1,12 @@
 ---
 title: Kakeya OProver Lab
-emoji: 😻
+emoji: 🧩
 colorFrom: indigo
-colorTo: pink
+colorTo: blue
 sdk: static
-pinned: false
+short_description: Lean proof-training journey and audited results
 ---
 
-Check out the configuration reference at https://huggingface.co/docs/hub/spaces-config-reference
+# Kakeya OProver Lab
+
+Static, token-free public report. No backend, GPU, paid hardware, telemetry, or external tracker.

app.js

@@ -0,0 +1 @@
+const q=s=>document.querySelector(s),qa=s=>[...document.querySelectorAll(s)];fetch('./data/results.json').then(r=>r.json()).then(d=>{q('#hero').textContent=d.hero;q('#cost').textContent=d.cost;const sel=q('#stage');d.stages.forEach(s=>sel.add(new Option(`${s.label} — ${s.status}`,s.id)));function draw(){const s=d.stages.find(x=>x.id===sel.value);q('#stagecard').innerHTML=`<h3>${s.label}</h3><p class="status">${s.status}</p><p>Strict exact: ${s.exact??'not qualified'}/22 · holdout ${s.holdout??'—'}/18 · canary ${s.canary??'—'}/4</p><div class="bar" aria-label="Exact Lean rate"><i style="width:${s.exact?100*s.exact/22:0}%"></i></div><p><a href="${s.repo}">Open model repository</a></p>`}sel.onchange=draw;draw();q('#stats').innerHTML=`<li>${d.statistics.parser}</li><li>Unsafe generations: ${d.statistics.unsafe}</li><li>${d.statistics.stage4_vs_stage2}</li><li>${d.statistics.stage4_vs_stage3}</li>`;q('#prod').textContent=`Converted ${d.production.converted}; canary ${d.production.canary}; ${d.production.scope}.`;q('#jensen').textContent=`${d.jensen.status}; Lean-valid ${d.jensen.lean_valid}; RH PROVED: ${d.jensen.rh_proved}.`;q('#taxonomy').innerHTML=d.failure_taxonomy.map(x=>`<li>${x}</li>`).join('');q('#artifacts').innerHTML=d.stages.map(s=>`<li><a href="${s.repo}">${s.label}</a></li>`).join('')+`<li><a href="${d.dataset}">Training dataset</a></li>`});qa('.tabs button').forEach(b=>b.onclick=()=>{qa('.tabs button').forEach(x=>x.setAttribute('aria-selected','false'));b.setAttribute('aria-selected','true');qa('.panel').forEach(p=>p.hidden=p.id!==b.dataset.tab)})

data/results.json

@@ -0,0 +1,66 @@
+{
+  "hero": "Production proof-advisor canary passed; Jensen theorem remained SEARCH_EXHAUSTED (0/6 Lean-valid). No RH proof.",
+  "stages": [
+    {
+      "id": "stage1",
+      "label": "SFT90",
+      "status": "NO-GO baseline",
+      "exact": null,
+      "repo": "https://huggingface.co/FluffyAIcode/Kakeya-OProver-Stage1-SFT90"
+    },
+    {
+      "id": "stage2",
+      "label": "SFT1000",
+      "status": "Matched baseline",
+      "exact": 9,
+      "holdout": 5,
+      "canary": 4,
+      "repo": "https://huggingface.co/FluffyAIcode/Kakeya-OProver-Stage2-SFT1000"
+    },
+    {
+      "id": "stage3",
+      "label": "DPO",
+      "status": "NO-GO regression",
+      "exact": 4,
+      "holdout": 1,
+      "canary": 3,
+      "repo": "https://huggingface.co/FluffyAIcode/Kakeya-OProver-Stage3-DPO"
+    },
+    {
+      "id": "stage4",
+      "label": "Repair SFT",
+      "status": "QUALITY GO / PROOF-ADVISOR-ONLY",
+      "exact": 10,
+      "holdout": 6,
+      "canary": 4,
+      "repo": "https://huggingface.co/FluffyAIcode/Kakeya-OProver-Stage4-Repair-SFT"
+    }
+  ],
+  "dataset": "https://huggingface.co/datasets/FluffyAIcode/Kakeya-OProver-Training",
+  "statistics": {
+    "parser": "22/22 for all matched evaluations",
+    "unsafe": 0,
+    "stage4_vs_stage2": "Not statistically significant (paired exact McNemar p=1.0).",
+    "stage4_vs_stage3": "Significant overall (p=0.015625) and on holdout (p=0.03125)."
+  },
+  "production": {
+    "converted": "504/504",
+    "canary": "12/12",
+    "scope": "proof-advisor canary only"
+  },
+  "jensen": {
+    "status": "SEARCH_EXHAUSTED",
+    "lean_valid": "0/6",
+    "rh_proved": "NO"
+  },
+  "cost": "Actual billed cost not provided by Jobs API.",
+  "failure_taxonomy": [
+    "parser/format",
+    "unknown identifier/import",
+    "type mismatch",
+    "rewrite no match",
+    "typeclass synthesis",
+    "unsolved goals",
+    "overlong generation"
+  ]
+}

index.html

@@ -1,19 +1 @@
-<!doctype html>
-<html>
-	<head>
-		<meta charset="utf-8" />
-		<meta name="viewport" content="width=device-width" />
-		<title>My static Space</title>
-		<link rel="stylesheet" href="style.css" />
-	</head>
-	<body>
-		<div class="card">
-			<h1>Welcome to your static Space!</h1>
-			<p>You can modify this app directly by editing <i>index.html</i> in the Files and versions tab.</p>
-			<p>
-				Also don't forget to check the
-				<a href="https://huggingface.co/docs/hub/spaces" target="_blank">Spaces documentation</a>.
-			</p>
-		</div>
-	</body>
-</html>
+<!doctype html><html lang="en"><head><meta charset="utf-8"><meta name="viewport" content="width=device-width,initial-scale=1"><title>Kakeya OProver Lab</title><link rel="stylesheet" href="styles.css"></head><body><main class="wrap"><header class="hero"><p class="status">PUBLIC SANITIZED RELEASE</p><h1>Kakeya OProver Lab</h1><p>Lean proof training from SFT90 to repair SFT, with matched strict evaluation and explicit non-claims.</p></header><nav class="tabs" aria-label="Report sections"><button data-tab='overview' aria-selected='true'>Overview</button><button data-tab='journey' aria-selected='false'>Training Journey</button><button data-tab='strict' aria-selected='false'>Strict Evaluation</button><button data-tab='metrics' aria-selected='false'>Training Metrics</button><button data-tab='failures' aria-selected='false'>Failure Taxonomy</button><button data-tab='production' aria-selected='false'>Production Qualification</button><button data-tab='jensen' aria-selected='false'>Jensen Result</button><button data-tab='repro' aria-selected='false'>Reproducibility</button><button data-tab='artifacts-panel' aria-selected='false'>Artifacts</button></nav><section class='panel card' id='overview' ><h2>Overview</h2><p id='hero'></p><label for='stage'>Stage selector</label> <select class='select' id='stage'></select><div id='stagecard' class='metric'></div></section><section class='panel card' id='journey' hidden><h2>Training Journey</h2><div class='timeline'><p>SFT90 — establish a small-data baseline.</p><p>SFT1000 — matched validity baseline.</p><p>DPO — preference optimization reduced strict validity.</p><p>Repair SFT — compiler-feedback repair restored quality gates.</p><p>Production alignment — 504/504 converted; 12/12 canary passed.</p></div></section><section class='panel card' id='strict' hidden><h2>Strict Evaluation</h2><ul id='stats'></ul><p class='muted'>Paired comparisons use exact McNemar tests; intervals are exact 95% confidence intervals on rates or discordant-pair win probability.</p></section><section class='panel card' id='metrics' hidden><h2>Training Metrics</h2><p>Loss curves and complete sanitized JSONL metrics are stored in each model repository. Stage selector above links to the source assets.</p></section><section class='panel card' id='failures' hidden><h2>Failure Taxonomy</h2><ul id='taxonomy'></ul><p>Repair SFT targeted executable-proof failures while rehearsing clean Mathlib examples.</p></section><section class='panel card' id='production' hidden><h2>Production Qualification</h2><p id='prod'></p><p>This is a proof-advisor qualification, not authorization for autonomous deployment.</p></section><section class='panel card' id='jensen' hidden><h2>Jensen Result</h2><p id='jensen'></p><p>No candidate proof bodies or production prompts are published.</p></section><section class='panel card' id='repro' hidden><h2>Reproducibility</h2><p>Immutable revisions, adapter hashes, dataset artifact hashes, protocol roots, audit digests, and public/private boundaries are in the bundled release manifest.</p><p id='cost'></p></section><section class='panel card' id='artifacts-panel' hidden><h2>Artifacts</h2><ul id='artifacts'></ul></section></main><script src="app.js"></script></body></html>

release-manifest.json

@@ -0,0 +1,183 @@
+{
+  "schema_version": 1,
+  "release": "Kakeya OProver public sanitized intermediate results",
+  "models": [
+    {
+      "schema_version": 1,
+      "public_repo": "FluffyAIcode/Kakeya-OProver-Stage1-SFT90",
+      "base_model": "m-a-p/OProver-8B",
+      "base_revision": "cd9ffd383b584d95bf00e04b88b35b05928b211c",
+      "source_private_repo": "FluffyAIcode/oprover-8b-mathlib-lora-stage1",
+      "source_immutable_revision": "cd091e33bc57f6c0f664846c6681b26d1163e411",
+      "adapter_sha256": "0b0770e31ad6e77b33742a5d68dfb48cc0fa67efae4c965aaa6309fd031a9b03",
+      "dataset_artifact_sha256": "eacefeab327a0d8c4b66e90b9afe9f7b8eb1df62c87abc9a1166f6b3e5ba8ced",
+      "public_private_boundary": {
+        "public": [
+          "adapter",
+          "tokenizer",
+          "sanitized metrics/trainer state",
+          "aggregate strict evaluation",
+          "hashes/signatures/config"
+        ],
+        "private": [
+          "chain-of-thought",
+          "production prompts",
+          "Jensen candidate proof bodies",
+          "raw candidate-bearing signed audits",
+          "optimizer and RNG checkpoints"
+        ]
+      }
+    },
+    {
+      "schema_version": 1,
+      "public_repo": "FluffyAIcode/Kakeya-OProver-Stage2-SFT1000",
+      "base_model": "m-a-p/OProver-8B",
+      "base_revision": "cd9ffd383b584d95bf00e04b88b35b05928b211c",
+      "source_private_repo": "FluffyAIcode/oprover-8b-mathlib-lora-stage1",
+      "source_immutable_revision": "8eead931f4b090bca2421fead7d0c64191bea116",
+      "adapter_sha256": "5e5399518c0741140a14d2cca2fade8ec3eb95fb587139c5c9894d5e297a3b55",
+      "dataset_artifact_sha256": "5ebec3f7ed71d0af202924ea9d5ca12a857c5363b89b028dbf74268bf2e32f24",
+      "public_private_boundary": {
+        "public": [
+          "adapter",
+          "tokenizer",
+          "sanitized metrics/trainer state",
+          "aggregate strict evaluation",
+          "hashes/signatures/config"
+        ],
+        "private": [
+          "chain-of-thought",
+          "production prompts",
+          "Jensen candidate proof bodies",
+          "raw candidate-bearing signed audits",
+          "optimizer and RNG checkpoints"
+        ]
+      }
+    },
+    {
+      "schema_version": 1,
+      "public_repo": "FluffyAIcode/Kakeya-OProver-Stage3-DPO",
+      "base_model": "m-a-p/OProver-8B",
+      "base_revision": "cd9ffd383b584d95bf00e04b88b35b05928b211c",
+      "source_private_repo": "FluffyAIcode/oprover-8b-mathlib-lora-stage1",
+      "source_immutable_revision": "c3b684ce7729ec94305deac4fbc5fd506c7f79a6",
+      "adapter_sha256": "064fb996230352ae12fd326944e8c5696edc22c36d34fc710805cb5aa2a3f9e3",
+      "dataset_artifact_sha256": "2de80cfbb1c5e14c89611810e02b9f432ec2643a203e4c983cd48b1e6ad919a3",
+      "public_private_boundary": {
+        "public": [
+          "adapter",
+          "tokenizer",
+          "sanitized metrics/trainer state",
+          "aggregate strict evaluation",
+          "hashes/signatures/config"
+        ],
+        "private": [
+          "chain-of-thought",
+          "production prompts",
+          "Jensen candidate proof bodies",
+          "raw candidate-bearing signed audits",
+          "optimizer and RNG checkpoints"
+        ]
+      }
+    },
+    {
+      "schema_version": 1,
+      "public_repo": "FluffyAIcode/Kakeya-OProver-Stage4-Repair-SFT",
+      "base_model": "m-a-p/OProver-8B",
+      "base_revision": "cd9ffd383b584d95bf00e04b88b35b05928b211c",
+      "source_private_repo": "FluffyAIcode/oprover-8b-mathlib-lora-stage1",
+      "source_immutable_revision": "7dd2e239e0857c6feb585f009e6118c511cc8e17",
+      "adapter_sha256": "a24765df00ba8213e0032c10cbcddb242a65ffee937520cea2b61bc0d2d68837",
+      "dataset_artifact_sha256": "54944619e3625f8a9db88b7c2a84507b86ea1dfc55f43d68f240dd9609244389",
+      "public_private_boundary": {
+        "public": [
+          "adapter",
+          "tokenizer",
+          "sanitized metrics/trainer state",
+          "aggregate strict evaluation",
+          "hashes/signatures/config"
+        ],
+        "private": [
+          "chain-of-thought",
+          "production prompts",
+          "Jensen candidate proof bodies",
+          "raw candidate-bearing signed audits",
+          "optimizer and RNG checkpoints"
+        ]
+      }
+    }
+  ],
+  "dataset": {
+    "schema_version": 1,
+    "public_repo": "FluffyAIcode/Kakeya-OProver-Training",
+    "mathlib_revision": "360da6fa66c1273b76b6b2d8c5666fd5ac2e3b56",
+    "configs": [
+      "sft-90",
+      "sft-1000",
+      "dpo-2000",
+      "repair-2800",
+      "strict-evaluation-22"
+    ],
+    "files": {
+      "sft-90/train.jsonl": {
+        "sha256": "7bd6d0822d80545ce2163aface7ba54484167394fdb38a4b11a3cd96e025b690",
+        "records": 63
+      },
+      "sft-90/validation.jsonl": {
+        "sha256": "f3eb510950b84d6cd52df91dce73b5314738f80d90b52ecf075276f09c34bd02",
+        "records": 9
+      },
+      "sft-90/holdout.jsonl": {
+        "sha256": "bfda01582726fe1a99daea87e7a7d1ba86e65526705a6fba8eb9e471df4680ab",
+        "records": 18
+      },
+      "sft-1000/train.jsonl": {
+        "sha256": "066b34aafe87c0da820c83781f6254d5c6a363bc93e5e44a65a501d8284885c5",
+        "records": 700
+      },
+      "sft-1000/validation.jsonl": {
+        "sha256": "804214d63ca01ad7abf3b2931147dc43057f6b2e7449480286cc89860ab592da",
+        "records": 100
+      },
+      "sft-1000/holdout.jsonl": {
+        "sha256": "7befdd6831a2b1e62a89b871022391565c0e965d83c2c9eac3f08741a37e8978",
+        "records": 200
+      },
+      "dpo-2000/train.jsonl": {
+        "sha256": "0e2a0a15d7ff03b5347a2e91da83c6c6d85539a44746c1d2d9662bc3e8ddde29",
+        "records": 1400
+      },
+      "dpo-2000/validation.jsonl": {
+        "sha256": "e478670e03df4af61532cf5954b06135816a2c7e8ea2bfab3e7109bac229c51c",
+        "records": 200
+      },
+      "dpo-2000/holdout.jsonl": {
+        "sha256": "1c97353d19ffe60dd436888123750c1d7f05a34445644ae8ad6f6ab23931c5f9",
+        "records": 400
+      },
+      "repair-2800/train.jsonl": {
+        "sha256": "1d4224ce24a29ec1069b8f56a0cb24598cc8c945ed0dfb74544428c4f5fba9d1",
+        "records": 2800
+      },
+      "repair-2800/validation.jsonl": {
+        "sha256": "f2a82d37dadf8a37fc20175339c9eea8ad0af91b7f2d32b3476a5a4abb90a6a6",
+        "records": 400
+      }
+    },
+    "excluded": [
+      "OProofs mixed/provenance-incomplete samples",
+      "production Jensen prompts and candidates",
+      "private reasoning and raw candidate-bearing audits"
+    ]
+  },
+  "space": "FluffyAIcode/Kakeya-OProver-Lab",
+  "collection_title": "Kakeya OProver — Lean Proof Training Journey",
+  "public_private_boundary": {
+    "public": "Adapters/tokenizers, approved Mathlib datasets and derived negatives, sanitized metrics/configs, aggregate evaluations, hashes/signatures, failure summaries.",
+    "private": "Original private repositories, private chain-of-thought, production prompts, Jensen candidate proof bodies, raw candidate-bearing signed audits, optimizer/RNG checkpoints."
+  },
+  "staging_scan": {
+    "file_count": 86,
+    "secret_scan_hits": 0
+  }
+}

styles.css

@@ -0,0 +1 @@
+*{box-sizing:border-box}body{margin:0;font:16px/1.55 system-ui,sans-serif;background:#08111f;color:#e6eefc}a{color:#8ec5ff}.wrap{max-width:1080px;margin:auto;padding:24px}.hero,.card{background:#111e31;border:1px solid #28405f;border-radius:16px;padding:24px;margin:16px 0}.hero h1{font-size:clamp(2rem,6vw,4.5rem);margin:.1em 0}.status{color:#86efac;font-weight:700}.tabs{display:flex;gap:8px;flex-wrap:wrap;position:sticky;top:0;background:#08111fee;padding:8px 0}.tabs button,.select{background:#172b46;color:#fff;border:1px solid #385b85;border-radius:9px;padding:10px 14px}.tabs button[aria-selected=true]{background:#27558a}.panel[hidden]{display:none}.grid{display:grid;grid-template-columns:repeat(auto-fit,minmax(220px,1fr));gap:12px}.metric{background:#0b1728;border-radius:12px;padding:16px}.bar{height:16px;background:#24364e;border-radius:8px;overflow:hidden}.bar i{display:block;height:100%;background:#60a5fa}.timeline{border-left:3px solid #60a5fa;padding-left:20px}.muted{color:#a9bad0}@media(max-width:600px){.wrap{padding:12px}.hero,.card{padding:17px}}:focus-visible{outline:3px solid #fbbf24;outline-offset:3px}