Learning to Reason with Insight for Informal Theorem Proving

Formal proof systems like Lean and Coq have dominated automated theorem proving for decades. They’re rigorous, verifiable, and theoretically sound. But there’s a problem: LLMs don’t think in formal logic. They think in natural language. When you force a language model to output Lean code, you’re asking it to translate its understanding into a syntax it never learned—one that humans struggle with too.

Los sistemas de pruebas formales como Lean y Coq han dominado la demostración automatizada de teoremas durante décadas. Son rigurosos, verificables y teóricamente sonido. Pero hay un problema: los LLMs no piensan en lógica formal. Piensan en lenguaje natural. Cuando obligas a un modelo de lenguaje a generar código Lean, le estás pidiendo que traduzca su comprensión a una sintaxis que nunca aprendió—una con la que los humanos también tienen dificultades.

This is the core insight behind Learning to Reason with Insight for Informal Theorem Proving (Li et al., 2026). The authors identify the real bottleneck in informal theorem proving: not proof generation—proof recognition. Models can write proofs. What they can’t do is recognize which technique to apply in the first place.

Esta es la idea central detrás de Learning to Reason with Insight for Informal Theorem Proving (Li et al., 2026). Los autores identifican el verdadero cuello de botella en la demostración informal de teoremas: no la generación de pruebas—sino el reconocimiento. Los modelos pueden escribir pruebas. Lo que no pueden hacer es reconocer qué técnica aplicar en primer lugar.

Here’s the analogy that hits home for anyone building agentic systems: A human mathematician doesn’t start by writing a formal proof. They look at a problem and think “this looks like a fixed-point theorem situation” or “we need induction here.” That’s insight—the pattern recognition that guides what to try before how to execute it. Current LLMs skip this step entirely. They dive straight into generation, and then wonder why they get stuck.

Aquí está la analogía que llega a casa para cualquiera que construya sistemas agénticos: Un matemático humano no empieza escribiendo una prueba formal. Mira un problema y piensa “esto parece una situación de teorema de punto fijo” o “aquí necesitamos inducción”. Eso es perspicacia—el reconocimiento de patrones que guía qué intentar antes de cómo ejecutarlo. Los LLMs actuales se saltan este paso por completo. Se lanzan directamente a la generación, y luego se preguntan por qué se atascan.

DeepInsightTheorem addresses this with a three-layer approach to the proof dataset. Instead of just storing full proofs, their hierarchical dataset structures each proof into: (1) Core technique—the mathematical insight or approach needed, (2) Proof sketch—the high-level strategy, and (3) Full proof—the complete execution. This explicit structuring forces the model to learn what the technique is, not just how to apply it.

DeepInsightTheorem aborda esto con un enfoque de tres capas para el dataset de pruebas. En lugar de almacenar solo pruebas completas, su dataset jerárquico estructura cada prueba en: (1) Técnica central—la perspectiva o enfoque matemático necesario, (2) Bosquejo de prueba—la estrategia de alto nivel, y (3) Prueba completa—la ejecución completa. Esta estructuración explícita obliga al modelo a aprender qué es la técnica, no solo cómo aplicarla.

But the dataset alone isn’t enough. The authors propose Progressive Multi-Stage SFT—a training strategy that mimics how humans actually learn. Stage 1: learn to write complete proofs. Stage 2: learn to identify and articulate the core technique before proving. It’s the difference between learning to solve problems and learning to recognize why a certain approach works.

Pero el dataset por sí solo no es suficiente. Los autores proponen Progressive Multi-Stage SFT—una estrategia de entrenamiento que imita cómo aprenden los humanos realmente. Etapa 1: aprender a escribir pruebas completas. Etapa 2: aprender a identificar y articular la técnica central antes de demostrar. Es la diferencia entre aprender a resolver problemas y aprender a reconocer por qué cierto enfoque funciona.

At inference, the model first outputs the core technique—essentially “here’s what we’re dealing with”—then generates the proof guided by that insight. It’s a two-step generation that mirrors the training, and the results speak for themselves: significant gains over baselines on miniF2F, PutnamBench, FIMO, and HMMT.

En inferencia, el modelo primero genera la técnica central—esencialmente “aquí es con lo que estamos tratando”—y luego genera la prueba guiada por esa perspicacia. Es una generación de dos pasos que refleja el entrenamiento, y los resultados hablan por sí mismos: ganancias significativas sobre los baseline en miniF2F, PutnamBench, FIMO y HMMT.

For agentic pipelines outside math, the lesson is clear: The bottleneck in complex reasoning isn’t execution—it’s direction. DSPy already teaches us this at the pipeline level: define what the signature should produce, compose modules that reason in different ways, and let optimizers tune the prompting. DeepInsightTheorem applies the same principle at the reasoning step level: teach the model to recognize which cognitive technique to deploy before generating.

Para pipelines agénticos fuera de las matemáticas, la lección es clara: el cuello de botella en el razonamiento complejo no es la ejecución—es la dirección. DSPy ya nos enseña esto a nivel de pipeline: define qué debe producir la firma, composa módulos que razonan de diferentes maneras, y deja que los optimizadores ajusten el prompting. DeepInsightTheorem aplica el mismo principio a nivel de paso de razonamiento: enseña al modelo a reconocer qué técnica cognitiva desplegar antes de generar.

This connects to Chain-of-Thought reasoning in a fundamental way. CoT assumes that if you ask a model to “think step by step,” it will naturally find the right steps. DeepInsightTheorem says that’s insufficient—steps are meaningless without insight into which approach to take. The hierarchy (technique → sketch → proof) is more effective than flat CoT because it separates strategic reasoning from tactical execution.

Esto conecta con el razonamiento Chain-of-Thought de manera fundamental. CoT asume que si le pides a un modelo que “piense paso a paso”, encontrará naturalmente los pasos correctos. DeepInsightTheorem dice que eso es insuficiente—los pasos son insignificantes sin perspicacia sobre qué enfoque tomar. La jerarquía (técnica → bosquejo → prueba) es más efectiva que CoT plano porque separa el razonamiento estratégico de la ejecución táctica.

The broader implication for building autonomous agents is this: Don’t just train models to output correct answers. Train them to recognize when to apply which technique. That’s the shift from ” autocomplete on reasoning” to “reasoning with insight”—and it’s what separates systems that scale from systems that plateau.

La implicación más amplia para construir agentes autónomos es esta: No entrenes solo a los modelos para generar respuestas correctas. Entrénalos para reconocer cuándo aplicar qué técnica. Ese es el cambio de “autocompletado de razonamiento” a “razonamiento con perspicacia”—y es lo que separa los sistemas que escalan de los que se estancan.

References

Referencias