Weekly Gallery
Latest edition
Aug 29 – Sep 5, 2026
Directions: 7 · Picks: 52
AI for Formal Math · Issue 4
Fermat's Last Theorem Machine-Verified in Lean
The biggest event this issue is the complete machine verification of Fermat's Last Theorem in Lean: Anthropic announced that Claude, in 11 days, on the Prove2Me…
Prove2Me: An Open Collaborative Platform for Scaling Math FormalizationProve2Me is the platform hosting the FLT formalization and the biggest community event this issue. Its key increment is decentralized open collaboration: a proof-sketches mechanism decomposes open theorems into atomic subproblems, cross-agent inheritance, an immutable Formalpedia corpus for reuse, and a mission mechanism where humans audit only the core while agents freely introduce intermediate lemmas. Compared to centralized swarm approaches, it removes single-organization compute bottlenecks and merge-queue serialization—essential for understanding how 'internet-scale formalization' can work.- SHADOWBENCH: Toward Reliable Automatic Evaluation of Semantic Alignment in AutoformalizationShadowBench uses a set of 'shadow theorems' with forward and backward implication checks to evaluate semantic alignment of auto-formalization, building the ShadowBench benchmark and achieving 98.8% expert agreement. Its increment: the shadow set is constructed once by experts and verified complete in Lean, enabling reusable evaluation of any generated result without over-reliance on reference phrasing; bidirectional implication simultaneously rejects weakened and strengthened statements, overcoming the defects of compile-rate and fixed-reference equivalence checks. Code and data are public—a must-read for auto-formalization evaluation.
- Reward-Oracle MCTS for Formal Theorem Proving: Sample-Efficient Search and the Need for Kernel-Level Proof AuditingThis work proposes a three-role MCTS framework that treats the Lean 4 compiler purely as a scalar reward oracle—UCB-guided tree updates do not feed error content back into the generation context, avoiding compiler-feedback contamination of the generation distribution. Its exhaustive axiom-level audit reveals proofs that depend on sorryAx yet pass standard checks, a key methodological increment for reliable evaluation. For those designing agentic proof search and verification pipelines, the kernel-level audit section is especially worth close reading.
Pretraining Data · Issue 4
New Frontiers in Document Corpora: Vision-Native Pretraining
On the document extraction quality axis, this issue presents a radical option that could reshape corpus construction decisions: instead of parsing PDFs into tex…
Scalable Visual Pretraining for Language IntelligenceAdvances the document extraction quality axis to "vision-native": during continued pretraining, directly use rendered PDF page images as input, train a shared autoregressive backbone with next visual latent prediction objective, without any text extraction or image-text paired supervision. Relative to Issue 2's "The Announcement Carries the Cue" (which treated structural cue encoding as a training variable), the increment is treating the "vision-native form of documents" itself as a training signal, demonstrating that with a 25% token budget on the same corpus, it surpasses text pretraining and improves cross-modal alignment; evidence comes from controlled comparisons at real scale on Qwen3.5 and Llama3.2 Vision backbones. Limitations: corpus recipe not disclosed, visual/text mixing ratios not systematically scanned, and criterion is post-SFT benchmarks without addressing RL trainability.- CausalMix: Data Mixture as Causal Inference for Language Model TrainingAdvances data mixture optimization from static regression to state-conditional causal marginal benefit estimation: uses DML/causal forests on 512 0.5B proxy runs to estimate CATE, and extrapolates to 7B and unseen data pools (LongCoT) without retraining proxies. Relative to RegMix-D's dynamic mixing in Issue 3, the increment is explicitly introducing data state covariates (complexity/difficulty/quality) and causal deconfounding, making the mixture strategy transferable to out-of-distribution data pools. Limitations: SFT setting (not pretraining) and code not released; should be referenced cautiously in pretraining contexts.
- DecoupleMix: Decoupled Ratio Search and Convex Allocation for Scalable VLM Data RecipesDecouples data mixture optimization into two orthogonal subproblems: inter-class proportion search and intra-class convex allocation, and proposes an attributable validation protocol for evaluating new dataset admission under fixed inter-class proportions and budget. Relative to RegMix-D's dynamic mixing in Issue 3, the increment is explicit two-level decoupling and attributable admission mechanism, and advances the evaluation unit from sample level to dataset level; evidence covers 2.5B–10B tokens and 32B models, with proxy-searched proportions transferring across scales without retuning. Limitations: only covers VLMs and data recipes not disclosed.
MoE & Sparse Experts · Issue 4
Routing Foresight Takes Over the System Layer: Predictive Placement and Micro-Step Scheduling
This issue focuses on the concentrated burst of "predictive" and "micro-step" ideas across the MoE system layer: routing replay extends from training-inference …
Director: Accelerating Distributed MoE Serving via Online Proactive Expert PlacementAdvances expert placement from "reactive afterthought" to "online foresight": predicts routing based on queued requests (via cascaded predictors or low-bit quantized replicas) to optimize expert layout in advance, overlaps migration with computation for near-zero-downtime reconfiguration, and centers on a polynomial-time (1+ε) approximate placement optimizer. Compared to Gimbal (cross-engine request scheduling) from Issue 3 and UltraEP (reactive rebalancing) from Issue 1, Director is the first to apply predictive replay ideas to intra-engine predictive placement, reducing end-to-end latency by 11–55% on Mistral/DeepSeek/Qwen.- Harnessing Routing Foresight for Micro-step-level MoE Load Balancing in RL Post-trainingTargets the unique load characteristics of RL post-training—stable at step level but volatile at micro-step level—by exploiting the fact that rollout routing is known before training. It proactively guides expert reconfiguration during recompute and policy update stages, decomposes the NP-hard problem into a four-stage planner, and uses CPU-assisted and GPU-direct complementary transmission paths to overlap migration. Compared to ReLibra from Issue 2 (which only optimizes policy update stage and uses GPU-direct only), ForeMoE's increment is optimizing the recompute stage and supporting expert migration, achieving up to 1.45× speedup over veRL on 64 GPUs.
- SMELT: Scaling Laws for Compute-Matched MoE Looped TransformersFirst to study MoE looped Transformers under three simultaneous budgets—per-token FLOPs, total parameters, and KV cache—fitting an independent Chinchilla-style scaling law and showing that looping still saves 6.8–18.0% training FLOPs under matched budgets. Compared to Slicing and Dicing from Issue 3 (sparsity-granularity decoupling), this paper introduces loop depth as a new scaling axis and provides a mechanism explanation (second-pass visits reduce attention sink, routing reuses a small core subset), extending sparse-structure scaling from "how wide" to "how deep."
Efficient Sequence Modeling · Issue 4
Sliding-window beats linear attention: the premise of post-training linearization is shaken
The strongest signal this issue comes from a counterintuitive negative result: Sliding-window beats linear attention is the first systematic comparison of post-…
Still: Amortized KV Cache Compaction in a Single Forward PassFirst to advance KV cache compression from per-context synthesis to amortized synthesis: using a per-layer Perceiver to synthesize compact key/value in a single forward pass, breaking the subset ceiling of selection methods and supporting iterative chunked compression for long-range scenarios. Relative to KV-Distill (amortized selection) and Cartridges/Attention Matching (per-context synthesis), its increment is achieving both synthesis and amortization, occupying the speed-quality frontier at 8x-200x compression and 8k-128k contexts, and exceeding the strongest baseline by 8-22 points on the long-context RULER grid, with real degradation evidence for cross-scale/architecture transfer and HELMET summarization retention.- Sliding-window beats linear attentionFirst systematic comparison of post-training linearized models against training-free sliding-window attention (with sink): SWA recovers 99% of baseline average performance on short-context tasks, is 2-10x higher on long-context reasoning, and requires zero post-training and zero specialized kernels. It directly challenges the premise of post-training linearization, corroborating the 'lazy large window' from Issue 1—efficient attention is more about optimization priors than long-range information carriers. Provides compute-matched controls from 1.3B to 70B and real degradation curves for S-NIAH/BABILong, a must-read negative result for anyone doing hybrid architecture or linearization research.
- Modern Transformers Are Implicit Hybrids: From Functional Differentiation to Principled Hybrid Architecture DesignUses interventional metrics RFIS/RPD to establish a complete dichotomous classification of retrieval heads and positional heads on the RoPE frequency axis, discovering a GPBand functional boundary that shifts with training length scale, and proposes head-granularity, layer-specific hybrid design principles (NoPE FA for global retrieval, LA for local positional modeling). Relative to Issue 2's 'Does RoPE Prevent or Degrade Retrieval Heads?' frequency-axis mechanism analysis, its increment is advancing frequency dependence from norm approximations to faithful interventional metrics, and directly instantiating it as a pre-trainable HwH hybrid architecture, with compute-matched controls for FA:LA<1:3 and zero-shot length extrapolation degradation curves.
Scaling Laws & Training Methods · Issue 4
Effective Learning Rate Becomes a Unified Coordinate, Muon Spectral Allocation Moves Toward Measurability
The most notable progress this issue is elevating the "effective learning rate" from a heuristic to a verifiable macroscopic coordinate. Effective Learning Rate…
Effective Learning Rate Governs Loss Dynamics in Language Model PretrainingElevates the effective learning rate η/‖W‖_F from a heuristic to a verifiable macroscopic coordinate: in 26 ELR-matched comparisons, loss trajectories collapse to a median error of 2.5×10⁻³, and it proves that the impact of weight decay and Hyperball (Issue 2) on loss is mainly realized through the ELR trajectory they induce, and enables fitted scaling laws to transfer across norm control methods (error reduced by 12.9×). Compared to the mechanistic analysis of On the Nonlinearity of Learning Rate Scaling from Issue 2, this is the first trajectory-level systematic validation, unifying "LR scheduling" and "norm control" as the same dynamical coordinate.- Spectral Allocation: Why Muon Outperforms Adam, and How to Improve MuonUses out-of-sample spectral probing to measure the loss-optimal step size in each singular direction of the momentum buffer, obtaining a stable anisotropic spectrum where "the head is at Edge-of-Stability, the body can tolerate larger steps," which uniformly explains why Muon outperforms Adam, which outperforms SGD, and proposes SAMuon/SAMuon-lite to amplify the body and anchor the head, saving 13.3–24% tokens relative to Muon at 124M–1B. Compared to the static spectral scaling law of Spectral Scaling Laws of Muon from Issue 3, this is the first per-rank out-of-sample measurement and static spectral prior, turning Muon improvements into measurement-driven design.
- Deriving Scaling Laws for OpenEuroLLM Models: Learning Rate, Batch Size and LossExtends the scaling of optimal learning rate and batch size to marginal settings (optimal LR for arbitrary batch and vice versa), and systematically studies the shift of optimal hyperparameters due to WSD annealing—annealing shifts the optimal LR up by up to 4×. Validates the Skaling law from Issue 1 over Chinchilla on open-source dense model suites. The increment lies in marginal scaling analysis and annealing-induced hyperparameter shifts, but the scale stops at 1.7B, so extrapolation to frontier scales requires self-assessment.
Coding Agents · Issue 4
Harness Anatomy and Multi-Day Autonomy
The engineering harness is substantially thickened as an empirical basis for the object of study. Harness Engineering provides the most complete source-level an…
Harness Engineering: Anatomy, Architecture, and Evolution of Coding Agents — A Source-Code Study of Eleven SystemsThe first source-level anatomy covering 11 production harnesses (including four provider-native systems) and the first meta-harness Omnigent, with controlled longitudinal diff across a quarter. Compared to Phase 3's Empire (three open-source harnesses), it expands the sample to include closed-source systems, adding longitudinal evolution and "platform shift" discourse, and is the most complete reference for engineering engineering.- Harness-of-Harness: Multi-Day Autonomous Software Development with Continual ImprovementOrganizes existing coding-agent harnesses into iterative planning-coding-testing loops with cross-loop state management (artifact state + evidence state), achieving multi-day autonomous development and continuous improvement, across three benchmarks, three harness-models, consistent gains (average relative +52%), and demonstrating 70+ iterations of multi-day FPS game development. Compared to Phase 3's SWE Refactor Bench's "one long-horizon task," it makes "continuous improvement" itself an evaluable object, with budget-controlled comparisons and ablations.
- Prompt-Induced Waste in Coding Agents: Reasoning, Effort, Harness Design, and End-to-End CostThe first pre-registered benchmark using prompt phrasing as an independent factor, quantifying prompt's impact on inference volume/verification behavior/end-to-end cost, giving "prompt, effort, harness are interaction factors, not independent controls" with CPS (cost per success) unified measurement. Compared to Phase 2's Scaffold Effect and Phase 1's Don't Blame the LLM, it adds prompt as a constant dimension, proving harness changes effort control (effort arm cost reduction from Claude Code's 19% to dsh's 75%).
Recursive Self-Improvement · Issue 4
Fragility of Self-Improvement Loops: From Pattern Collapse to Non-Transferable Improvements
The main theme of this issue is the fragility of self-improvement loops. Last issue, we localized failures to the self-evaluation stage; this issue, we see the …
Beneath the Diff: Diagnosing and Mitigating Algorithmic Mode Collapse in Code-Level Autonomous Research LoopsIdentifies a previously undocumented failure mode in code-level autonomous research loops—"algorithmic pattern collapse": the agent continues editing different lines of code, but diversity at the semantic and mechanistic levels collapses, repeatedly proposing the same algorithmic change, while the gap between in-loop metric gains and held-out evaluation gains widens. Compared to the execution/learning-side patch taxonomy in Issue 2 [AI4AI-Bench], this advances the diagnosis to the more insidious failure of "surface diversity stable but semantic collapse," and uses a three-layer protocol (in-loop / audit / blind) to separate optimization signals from true generalization; the DAPS mitigation reduces semantic cluster decay by 69.1% and improves blind-test fidelity by 83.7%. Read it to understand why "edits change, ideas don't" is the most insidious degradation of the loop.- Falsifiable Release Gates for Self-Improving Systems: Standing Invariants at ScaleTransforms safety claims for self-improving systems from "self-assessed README promises" to "falsifiable release gates": every new capability must pass a pre-declared, machine-checkable acceptance suite before release, and a set of standing invariants holds across gates. The core is "teeth discipline"—each invariant is paired with a deliberately broken model that the checker must be able to reject, proving the checker has real power; the authors have run the runtime through seven releases with zero changes to invariants, and one release added capabilities without needing new invariants. Compared to the trajectory reproducibility standard in Issue 2 [Rollout Cards], this provides the falsifiability requirement itself—"the checker can fail." Read it as the engineering answer for the governance layer of self-improvement loops.
- On the Fragility of Self-Improving Agents: Variance, Task Order, and UnderspecificationConducts multi-run and shuffled-task stress tests on two memory-based self-improvement methods (AWM, RBank), exposing two reliability issues masked by single-run reports: in 71% of cases, self-improvement loops amplify run-to-run variance (best vs. worst can differ by 10 percentage points), and performance flips from +1.5% to -4.5% under shuffled task orders—the default task order is an implicit curriculum, a hidden prerequisite for success. The diagnosis identifies task/environment underspecification as a key cause, but adding rubrics and environment feedback only closes 31% of the degradation gap. Compared to the transfer-level null in Issue 2 [Phantom Gains], this advances "single-run untrustworthiness" to "task order itself is a hidden prerequisite." Read it to design controls for any self-improvement loop.