Four programs, one standard of rigor.

In people, the ability to hold and manipulate a sequence in working memory (for instance, repeating digits backward) predicts performance on abstract-reasoning tests like Raven's matrices. We ask whether the same link exists in large language models, and if so, what mechanism carries it.

The program pairs a cross-model behavioral battery with causal interventions inside individual networks: linear probes and information estimates on hidden states, targeted attention-head ablations, activation patching, and steering. Experiments are preregistered, models are pinned to exact revisions, and runs execute on rented A100/H100/B200 GPUs and Dartmouth's Discovery cluster.

• Scope25+ open-weight models across dense, mixture-of-experts, and hybrid architectures.
• MethodBehavioral battery, probes, head ablations, activation patching, steering.
• CollaborationConducted with Dartmouth's cognitive science faculty.
• ToolingOpen-source subspace-intervention toolkit on GitHub.

A lattice point is visible from the origin when nothing blocks the straight line to it; classically, a fraction 6/π² ≈ 61% of points are visible. Chaubey and Pandey asked what happens along curves y = t·F(x), and conjectured that almost every point becomes visible once F has two distinct roots.

Our first paper (with Tristan Phillips) proved this for every power fᵐ of such a polynomial, with a quantitative bound via Pila's theorem. A second pins down the exact order of growth, N log N, of the invisible set for powers of quadratics. A third, sole-authored paper proves density one for every nonzero integer polynomial with at least two distinct roots, resolving the generalized conjecture for nonzero polynomials.

• HeadlineD(F) = 1 for every nonzero F ∈ ℤ[x] with two distinct roots.
• SharpnessThe two-root hypothesis cannot be dropped.
• Quantitative#Invisible(N) ≍ N log N along (Ax² + Bx + C)ᵐ, m ≥ 3.
• VerificationThe density-one theorem is fully machine-checked in Lean 4.

Our density-one theorem for lattice-point visibility is formalized in Lean 4 against Mathlib: roughly 2,000 lines across 16 modules and 74 theorems and lemmas, with no sorry placeholders and only Lean's standard axioms. The formal statement is the paper's main theorem.

We use AI systems openly in proof search, formalization, and drafting, and disclose that use in our papers. The proof assistant is what makes this safe: a result is accepted only when the kernel checks it.

• Scale≈1,980 lines · 16 modules · 74 theorems.
• Trust basepropext, Classical.choice, Quot.sound only.
• ToolchainLean 4.28 · Mathlib.
• StatusPublic, reproducible build.

qwen-harness runs a 35B-parameter mixture-of-experts model as a local tool-calling agent on Apple Silicon. DFlash speculative decoding, a multi-turn prompt-cache patch for the model's hybrid attention layout, and mixed 8/4-bit KV caching raise decode throughput 37–45% on long prompts while cutting memory use by about 3 GB.

Around the model sits an agent stack designed for reliability: an audit gate that checks numeric claims against tool outputs before they reach the user, a loop guard, compact tool schemas (about 7× smaller), and an evaluation driver for financial-analysis tasks.

• Throughput+37–45% decode speed on 3K–9K-token prompts.
• Latency0.12 s streaming time to first token.
• Memory≈3 GB saved with mixed-precision KV cache.
• Quality34 tests; finance-agent evaluation suite.