Weekly Gallery
Latest edition
Sep 19 – 26, 2026
Directions: 7 · Updated this issue: 3 · Picks: 18
AI for Formal Math · Issue 7
Long-Horizon Formalization Crosses into Research-Level Mathematics: Fermat's Last Theorem, MIP*=RE, and Ramsey
The main thread of this issue is the transition of long-horizon automated formalization from proving individual theorems to formalizing entire research papers a…
Long-horizon autoformalization of a core theorem underlying MIP*=RE (FormalFlow)FormalFlow completed a 126,367-line Lean 4 formalization of the core theorem of MIP*=RE (quantum soundness of the classical low-individual-degree test) in 63 days, with no sorry and using only standard axioms. Compared to Issue 2's LeanMarathon and Goedel-Architect, its increment lies in explicit governance of "statement drift" and "proof composition": shared blueprint, nested feedback loops, a proof-gap protocol distinguishing paper corrections from formalization fixes, and hardening failure modes found in review into automated CI checks. The 25 gap notes corrected errors in published theorem statements and error budgets; the public repository, blueprint, and development history make it a reproducible artifact.- (Auto)formalization is supposed to be easy: Trellis process semantics for spelling out rigorous proofsTrellis uses a deterministic process kernel (35k lines of Rust + TLA+ specification) to operationalize "rigor" as machine-checkable monotonic refinement: three verification channels (substantive, correspondence, reliability) plus fingerprint reopening, with human-approved semantic closure making faithfulness independent of agent reliability. Compared to LEAP, Goedel-Architect, and Magenta, which rely on LLM judgment or training, Trellis makes "progress" a checkable property of tablet state, using off-the-shelf models to end-to-end formalize two recent Ramsey papers (including work breaking a 50-year exponential barrier), with complete cycle checkpoints public.
- Learning to Discover Interesting MathematicsGives the first computable, library-grounded definition of "intrinsic interestingness"—the ratio of proof length to statement description length—and proves its strong correlation with downstream utility (Spearman 0.756). Trains a 27B model to predict conditional proof difficulty, outperforming frontier general-purpose models; using interestingness as a reward to guide conjecture models reduces overlap of generated theorems with Mathlib from 91.9% to 30.6%, providing a discovery signal for self-extending formalization libraries without human targets. Compared to Stellar Colosseum's multi-agent orchestration, its increment is an optimizable quantitative objective.
Pretraining Data · Issue 7
Data Selection Begins to Use RL Coverage as Criterion
The clearest signal this issue is that the "post-training upper bound" criterion has moved from diagnosis to actionable intervention. TailSFT shifts the goal of…
TailSFT: Filtered Fine-Tuning Improves Post-Training PerformanceShifts SFT data filtering from "improving single-sample accuracy" to "preserving coverage for subsequent RL": using the initial policy as a reference, it filters already-fitted sequences based on loss reduction, and provides a coverage ratio diagnostic to predict when filtering will be effective. Relative to Issue 5's "Good Pretraining, Bad SFT," which treated "optimal base loss does not equal optimal post-training" as a diagnostic conclusion, the increment here is advancing that criterion into an actionable SFT intervention, validated at the 7B scale with GRPO-matched controls: filtered checkpoints have lower pass@1 before RL but higher pass@1 in every comparison after RL (up to +3.9%), and 10 out of 11 settings with ρ16>1 have non-negative coverage gains. Limitations: does not address pretraining corpus composition itself, and filtering ratios are not systematically scanned.- Building Multilingual Bridges: Data Mixing as the Pillar of Generalization for In-Language ReasoningFirst systematic study of the impact of data mixing and scheduling in the SFT stage on the generalization of "reasoning in the prompt language," providing evidence at the 3.35B scale that multilingual non-reasoning data is a cheap lever for cross-lingual transfer: there is a sweet spot of 20–30% for the proportion of non-reasoning data (0%→10% raises reasoning rate on unseen languages in MGSM from 46% to 89%, and accuracy from 49% to 67%), and data mixing outperforms sequential adaptation and weight merging. Relative to Issue 6's MiST synthetic mid-training corpus design, the increment is treating "reasoning language" itself as a trainable behavior and providing a ratio sweet spot; public model weights and multilingual reasoning data are released. Limitations: scale is 3.35B and the criterion is post-SFT benchmarks.
- When Data Is Scarce: Scaling Sparse Language Models with Repeated TrainingFirst to explicitly couple dynamic sparse training (DST) with data-constrained repeated training, providing sparse-aware data-constrained scaling laws, finding that moderate sparsity (~50%) delays the repeated data saturation point from R_d*=4.4 to about 6.9, and giving a separation between loss-optimal (~50%) and compute-optimal (higher and increasing with data scale) sparsity. Relative to Issue 5's "Data Scarcity and Model Sparsity," which focused on mechanistic analysis of MoE sparsity and repetition harm, the increment is providing extrapolable scaling law functional forms and resource allocation prescriptions for DST; code is public with sensitivity analysis. Limitations: scale stops at 1.92B fitting/7.68B extrapolation, criterion is validation loss, and DST is not the default pretraining paradigm.
Efficient Sequence Modeling · Issue 7
Diversification of Selection Signal Sources and the Dispute over Sink Origins
The strongest signals this issue are the simultaneous advancement of cross-layer KV sharing and the diversification of selection signal sources. HySparse2 unifi…
HySparse2: Hybrid Sparse Attention with Two-Level KV SharingUnifies YOCO-style cross-layer KV sharing (KV Bridging) with intra-block KV reuse (KV Reuse) into a two-level sharing scheme, and for the first time places token-level sparse selection and forced local windows into the same KV cache, allowing prefill to fully early-exit after the self-decoder. Relative to the cross-layer KV and index reuse of DeepSeek-V4.1-Flash from Issue 6, the increment is jointly covering both inter-layer sharing and token-level selection dimensions, providing compute-matched comparisons and degradation curves on RULER-v2/MRCR-v2/AgentPPL/LongPPL for 80B-A3B/290B-A8B; the comparison between KV Bridging and KV Mirror also reveals the advantage of full-attention layers as KV sources.- Complex KDA: Understanding and Enhancing the Expressivity of Kimi Delta AttentionBy relaxing the KDA gate to [-1,1] and the delta rule coefficient to [0,2], a single diagonal-plus-rank-one transition can implement 2D rotations and complex eigenvalues, proving that every orthogonal DPR1 matrix is exactly a CKDA transition. Relative to the scalar gates of DeltaNet/GDN, the increment is showing that channel-wise gates themselves can provide reflections, avoiding extra rank-one updates, and a single layer can track all finite subgroups of SO(3) (including A5) with one fewer layer than GDN. Provides compute-matched comparisons and scaling analysis for state-tracking and language modeling, but long-context evaluation is limited to periodic waveform continuation.
- Language Models Can Control Their Own AttentionFor the first time advances the selection signal for sparse attention from internal activations/proxy scores to an explicit text protocol declared by the model: the model outputs <global>/<focus>/<local> tags in the CoT, and the inference engine dynamically constructs block-level masks accordingly, completely eliminating the per-query O(N) selection cost. Relative to the trainable Forecast indexer of SparDA from Issue 1 and the query-group shared index of PIVOT from Issue 6, the increment is making selection itself part of the model's output (system-2 sparse attention), with zero training, zero auxiliary scorers, and providing compute-matched comparisons and degradation curves across 15 tasks and multiple model scales. The limitation is that the zero-shot protocol adds about 1/3 decoding steps and efficiency claims are based on roofline.