Spaces:
Running
Running
File size: 4,994 Bytes
81674f5 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 | <!doctype html>
<html lang="en">
<head>
<meta charset="utf-8">
<meta name="viewport" content="width=device-width,initial-scale=1">
<title>Claims 4 and 5 — formal verification poster</title>
<style>
/* ===== DESIGN TOKENS ===== */
:root {
--paper: #f7f4ec;
--ink: #102a2a;
--muted: #566768;
--accent: #0d7773;
--accent-soft: #d8eeea;
--warn: #a64b2a;
--white: #ffffff;
--line: #c6d5d1;
--shadow-card: 0 10px 24px rgba(16,42,42,.08);
--fs-1: 14px;
--fs-2: 18px;
--fs-3: 23px;
--fs-4: 34px;
--fs-5: 58px;
--fs-6: 72px;
--font-serif: "Georgia", serif;
--font-sans: "Inter", "Helvetica Neue", sans-serif;
}
/* ===== END DESIGN TOKENS ===== */
@page { size: 16in 9in; margin: 0; }
* { box-sizing: border-box; }
body { margin: 0; background: var(--paper); color: var(--ink); font-family: var(--font-sans); }
.poster { width: 1600px; min-height: 900px; padding: 56px 64px 44px; display: grid; grid-template-rows: auto auto 1fr auto; gap: 26px; }
.masthead { border-bottom: 5px solid var(--accent); padding-bottom: 22px; }
.eyebrow { color: var(--accent); font-size: var(--fs-2); font-weight: 800; letter-spacing: .12em; text-transform: uppercase; }
h1 { font-size: var(--fs-5); line-height: 1.02; max-width: 1320px; margin: 10px 0 0; letter-spacing: -.035em; }
.hero { display: grid; grid-template-columns: 1.2fr .8fr; gap: 24px; }
.result { background: var(--accent); color: var(--white); padding: 26px 30px; border-radius: 18px; }
.result strong { display: block; font-size: var(--fs-6); line-height: 1; }
.result span { display: block; font-size: var(--fs-3); margin-top: 10px; }
.guardrail { border: 3px solid var(--warn); color: var(--warn); padding: 24px 28px; border-radius: 18px; font-size: var(--fs-3); font-weight: 750; }
.grid { display: grid; grid-template-columns: 1fr 1fr 1fr; gap: 24px; align-items: stretch; }
.card { background: var(--white); border: 2px solid var(--line); border-radius: 18px; padding: 26px 28px; box-shadow: var(--shadow-card); }
.card h2 { font-size: var(--fs-4); margin: 0 0 15px; }
.card p, .card li { font-size: var(--fs-2); line-height: 1.42; }
.card ul { padding-left: 23px; margin: 10px 0 0; }
.tag { display: inline-block; background: var(--accent-soft); color: var(--accent); border-radius: 999px; padding: 7px 13px; font-weight: 800; font-size: var(--fs-1); }
.metric { color: var(--accent); font-size: var(--fs-4); font-weight: 850; margin: 13px 0 4px; }
.risk { color: var(--warn); }
footer { display: flex; justify-content: space-between; border-top: 2px solid var(--line); padding-top: 18px; font-size: var(--fs-1); color: var(--muted); }
code { font-family: var(--font-sans); }
</style>
</head>
<body>
<main class="poster" data-measure-role="poster">
<header class="masthead" data-measure-role="header">
<div class="eyebrow">ICML 2026 reproduction · arXiv:2602.15503</div>
<h1>Universal approximation evidence moves from chosen examples to a Lean-checked compact-space theorem</h1>
</header>
<section class="hero">
<div class="result">
<strong>2 / 2</strong>
<span>formal negative controls rejected; all target theorems compile</span>
</div>
<div class="guardrail">Live score remains 8/10 until the judge evaluates this revision. Claim 4 still carries one explicit formalization boundary.</div>
</section>
<section class="grid" data-measure-role="body">
<article class="card">
<span class="tag">CLAIM 5 · HIGH</span>
<h2>Arbitrary compact spaces</h2>
<div class="metric">7 theorem obligations</div>
<ul>
<li>strict-margin scaling</li>
<li>two compact finite subcovers</li>
<li>lattice min/max envelope</li>
<li>product Lipschitz budget</li>
</ul>
<p>No chosen target, target-derived basis, or finite sampling.</p>
</article>
<article class="card">
<span class="tag">CLAIM 4 · MEDIUM</span>
<h2>Universal deduction</h2>
<div class="metric">Lean 4.19.0</div>
<p>The kernel derives uniform approximation for every separately Lipschitz target and every positive tolerance from nonempty, lattice-closed, strictly interpolating paper-class premises.</p>
<p class="risk"><strong>Boundary:</strong> exact matrix-level realization of those premises is source-audited, not yet encoded in Lean.</p>
</article>
<article class="card">
<span class="tag">REPRODUCIBLE</span>
<h2>One fixed command</h2>
<div class="metric">164.07 s</div>
<p><code>uv run --frozen python run_reproduction.py</code></p>
<ul>
<li>mathlib v4.19.0</li>
<li>no <code>sorryAx</code></li>
<li>only standard axioms reported</li>
<li>HF cpu-upgrade, one worker</li>
</ul>
</article>
</section>
<footer data-measure-role="footer">
<span>Evidence SHA <code>3820f7a5601f0d4e52d1936ce045303796519f8d</code></span>
<span>DineshAI/OVBpXUvwMi · Job 6a6c0f3023ed89c748ec8e1f</span>
</footer>
</main>
</body>
</html>
|