Research

An int8 copy of the LM head bounds every vocabulary score. The head recomputes only the entries that could win and falls back to the engine’s head when the bounds leave the token undecided.

Every token matches the engine head on the same batch in replay and when served beside the stock head. Drafter-head bounds skip almost no vocabulary in the tested variants.

The certification theorem assumes a tested but unproved error model of the closed-source production kernel.

Small sampled hulls organize keys into simplicial normal cones. Dyadic bins share moment sums across queries, while conflict sets recurse; reconstruction uses exact integer arithmetic.

A time cutoff gives the error and running-time guarantee with probability at least 2/3. Without a cutoff, every execution meets the error bound and the running-time bound holds in expectation.

A Lean formalization (103 audited theorems) proves Lemmas 4.1 and 5.1 and parts of Lemmas 2.1–3.2 and 4.2. Facts about the sampled hull enter as hypotheses, and the assembly into Theorem 1.1 is not formalized.

A proof counts algebraically independent kernel ratios recoverable from output derivatives. Each cache epoch contributes only a bounded number of Jacobian generators, even with recomputation and finite branching.

Theorem 5.5 proves Ω(nd + n²d²/M) transfers when every exponential argument is a polynomial in the full dot-product scores, including mixtures that form no individual score.

Lean 4 proofs cover Lemmas 2.1, 2.2, 4.1, 5.1 and 5.4 and Theorem 5.2. The passage from a program to its trace and the transfer counts of the constructions are not formalized. Field containment alone does not give uniform dependence on d: a Strassen-based prefix reaches the full attention coefficient field in o(nd + n²d/M) transfers on a parameter sequence while computing only an auxiliary vector.

For tanh networks with zero biases and absolute row sums at most one, the expected number of input queries scales as the square root of depth at each fixed first-layer rank. A uniformly bounded column envelope gives the same scale at any rank, in the logarithmic-depth, finite-precision regime.

The decoder's outputs follow the original autoregressive law exactly. Fixed-rank depth sharpness requires sufficient width and coefficient precision; the unrestricted square-root versus linear query gap remains open.

These bounds give no useful speed prediction at the large ranks of ordinary models. Lean checks some theorems in full and, for others, the analytic core or the closing arithmetic under stated hypotheses. Bit complexity, preprocessing, storage and runtime are not formalized.

The paper compares how far attention can be compressed with what a certificate needs to read, using reachable states of frozen SmolLM2-135M.

At a 7,168-token prompt, exact packing witnesses for the certificate need at least 28.88% of dense final-layer interactions. A concrete tenfold grouping has a checked one-intervention sequence total variation of 1.148 × 10⁻⁵.

The public replay and arithmetic checks pass. Lean checks six supporting arithmetic lemmas; the main argument and the PyTorch code are outside the formalization.

When can a summary certify an attention result without reading every cached row? StateCut sharpens the bounds with exact row counts, refines inconclusive summaries in a persistent forest, and makes decoder writes transactional. Results are checked against an explicit numerical reference.

The checks include 66 Lean theorems and 68,851 GPU arithmetic cases. In small synthetic examples, the finite-count bounds avoid raw-row reads.

The paper asks what compressed moment information can determine about attention outputs. It combines exact boundary certificates, value coupling, rational test cases, and GPU measurements that include the cost of decisions and fallback.

Coupled bounds accept 61 of 149 initial coordinates in the constructed rational suite, versus 57 for independent boxes.

Sampling from an unknown member of a known finite class using approximate prefix masses, with every query to the guide charged.

Under pointwise guidance with factor 9/4 and error 1/16, worst-case query complexity is min{M, n√(log M), n²} up to logarithms. A known background plus an unknown atom has a matching worst-case rate over backgrounds at error at most α/4; a uniform background permits a sharper rate.

Lean 4 formalizes the numbered results with the cited finite-class upper bound taken as an explicit hypothesis. The general fixed-error finite-class gap remains open.

A rectangle-based learner uses logarithmically many statistical queries at constant tolerance, while the same classes require dimension linear in the construction scale.

The dimension lower bound survives allowing the feature law to depend on a known target prior and discarding any fixed fraction of targets below one. The classes also give a counterexample to the stated representation bound in Karchmer and Malach’s Theorem 4.1, whose proof Feldman et al. (2026) had already reported as flawed.

The counterexample does not disprove Karchmer and Malach’s broader mini-batch SGD conclusion.

The paper studies exact single-example logistic SGD on a two-layer bias-free ReLU network, with Gaussian initialization and tail-sum prediction. Learning to error below one-half under every input marginal forces a kernel margin.

The kernel margin yields VC-dimension and deterministic representation bounds. Above an explicit dimension threshold, only constant targets can be learned under every marginal. Separate results cover parity and fixed-gate updates.

Lean checks the risk bound, margin theorem and fixed-gate theorem, except the final random-projection step. The other results are proved in the paper.

Fair-bit noise smooths rare events, a polynomial approximates the transformed logits, and a robust logit learner runs on a cached sampling simulation. A second proof uses a surrogate with low probability rank.

At fixed accuracy and confidence, the bound on submitted and generated tokens has degree 6d + 15 in T, up to logarithmic factors and rank-dependent constants. A supplied inverse-polynomial conditional-probability floor permits joint polynomial learning in T and d. If the rank can grow, no learner is polynomial in both T and d, assuming strong pseudorandom functions computable by logarithmic-depth circuits once the key is fixed.

Numerical logit simulation can require exponentially many samples even at rank one. Lean takes the cited learning and compilation guarantees as hypotheses and does not cover the pseudorandom-function assumption, the coupling of cached estimates, running time or bit complexity.

A null-clone reduction bounds likelihood sums by candidate count and constructs a finite rational dominating pair that composes across epochs. The accountant allows heterogeneous items and queries that adapt to earlier releases.

For 1,000 batches per epoch, five epochs, noise multiplier 1 and δ = 10⁻⁸, the worst-case ε lies in (6.423, 7.97]; matched Poisson sampling is certified at 0.507. An adaptive counterexample shows that the pair Chua et al. conjectured to dominate all adaptive queries does not.

Lean covers the dominating-pair construction, counterexample and supporting certificate lemmas. The reduction and other stated steps remain in the written proofs.

A SQL agent learns reusable relations from correct queries, corroborates them on later tasks, and executes them in new computations without updating model weights.

A 240-episode diagnostic used 40.9% fewer tokens than full history, but 115.4% more than the ACE baseline, with every arm at the accuracy ceiling.

The paper studies closed quantum machines that transform fresh inputs while returning their memory to its initial state, including exact and approximate return and repeated use of the coherent quantum homogenizer.

Exact memory return prevents a closed machine from purifying maximally mixed inputs. With return tolerance δ, exact purification of n qubits needs n/δ + O(n) memory qubits, while independent randomization needs only ⌈n/2⌉. For the coherent quantum homogenizer, requiring independent outputs and return after every use forces ϵ + δ/2 ≥ 1/4.

Lean proofs cover the soundness of the disjoint-gate exchange certificates and the first-use step of Proposition 14.

Two force-weighted cross responses bound the spin channel through the shared support. Classical force replay measures the bound, and local pulse changes can null both responses.

When gravity acts mainly during a hold, the permissible pulse-weighted compliance scales as the cube of the ramp time. A modeled clamped horizontal link gives a phase comparable to a millisecond-ramp gravitational reference and a negligible one for long ramps.

The calculations are checked by 57 unit tests and two interval checks.

The paper derives consistent exclusivity and Bell bounds from information tasks, without assuming a quantum state space in the task proofs.

Completing two-copy parity measurements with an “other” outcome gives a Bell bound controlled by the weights of the residual records. No-hypersignaling supplies the capacity bound when the relevant preparations are accessible and local signaling dimensions match the label counts.

The examples and certificates pass 1,276 exact finite checks. The general task arguments are proved in the text.

Do finite work and heat tasks determine a single additive entropy? The paper studies a modified pair-task formulation with sharp work stores and exact return of the machine’s memory marginal.

In an energy-conserving quantum completion, mean energy and von Neumann entropy determine closed tasks, and entropy alone determines work-assisted tasks. A known no-broadcasting theorem excludes coherence between distinct energies when comparison and convexity are required.

The construction gives one entropy model. The paper does not show that every compatible dynamics has the same entropy order. Both finite programs pass their classical and exact quantum checks.

• Sunflower constructions · Erdős 20

  Lean developments for extremal families, kernel reductions, recurrences, and tensor arguments.

• Partial results · Erdős 885

  Five explicit anchored witnesses refute a proposed cap of four, and a finite sieve identifies four common positive factor differences for a guidepost triple.

• Erdős–Hajnal obstructions · Erdős 61

  Explicit obstructions to affine-shadow, path-profile, and blockade reductions, with selected proof cores formalized in Lean.

• Working formalizations · Erdős 119

  Dyadic rigidity, defect budgets, and counterexamples collected in Lean.