Demostración automática de teoremas con IA y verificación formal en Lean 4

Informe técnico

Estado a agosto de 2026

0. Arquitectura del stack

Cuatro capas, con lógicas distintas y responsabilidades separadas:

El invariante del sistema es que solo la capa 0 tiene autoridad. Las capas 1–3 pueden estar rotas sin comprometer la corrección: si el elaborador infiere mal, el hammer traduce mal o el LLM alucina, el término producido no tipa y se rechaza. Esto es lo que hace de Lean un entorno de RL con recompensa binaria fiable.

I. La lógica

I.1 El kernel: CIC

Lean 4 implementa el Cálculo de Construcciones Inductivas con extensiones. Componentes:

Jerarquía de sorts

Prop := Sort 0
Type u := Sort (u+1)
Sort u : Sort (u+1)

• No acumulativa: α : Type 0 no implica α : Type 1. Hay que usar ULift para subir de universo, con el coste de tener que transportar todo explícitamente.
• Polimorfismo de universos: las constantes se declaran con parámetros de universo {u v} y se instancian en cada uso. El elaborador resuelve restricciones de universo mediante un solver de desigualdades sobre expresiones max/imax.
• La jerarquía existe por la paradoja de Girard: Type : Type permite derivar False.

Prop impredicativa

Prop es impredicativa: ∀ (α : Type u), P α : Prop sigue estando en Prop, sin importar u. Esto es lo que permite cuantificar sobre todos los grupos dentro de un enunciado que sigue siendo una proposición.

Regla de formación (imax):

Γ ⊢ α : Sort u    Γ, x : α ⊢ β : Sort v
----------------------------------------
Γ ⊢ (x : α) → β : Sort (imax u v)

donde imax u 0 = 0. Ese caso especial es la impredicatividad de Prop.

Irrelevancia definicional de pruebas

Si h₁ h₂ : p con p : Prop, entonces h₁ ≡ h₂ definicionalmente (no solo proposicionalmente). El kernel las identifica sin prueba. Consecuencias:

• Las pruebas no tienen contenido computacional extraíble (no hay extracción de programas desde Prop, a diferencia de Coq/Rocq donde esto es un uso central).
• Los subtipos {x : α // p x} tienen igualdad determinada solo por la componente de valor: Subtype.ext.
• Es una de las dos causas de que el tipado no sea del todo decidible (§I.4).

Tipos inductivos

Familias inductivas con eliminadores generados automáticamente. El kernel genera, para cada declaración inductive, los constructores, el recursor T.rec y las reglas de reducción-ι. Ejemplo:

inductive Vec (α : Type u) : Nat → Type u where
  | nil  : Vec α 0
  | cons : α → Vec α n → Vec α (n+1)

El chequeo de positividad estricta rechaza definiciones como inductive Bad where | mk : (Bad → Bad) → Bad, que darían inconsistencia.

Eliminación de subsingletons: normalmente un inductivo en Prop solo puede eliminarse hacia Prop. Excepción: si el inductivo tiene a lo sumo un constructor y todos sus argumentos son proposiciones o aparecen en la conclusión, se permite eliminar hacia Type. Esto es lo que hace usable Acc (accesibilidad) para definir recursión bien fundada.

Cocientes

Quot es primitivo del kernel, no derivado:

Quot     : {α : Sort u} → (α → α → Prop) → Sort u
Quot.mk  : (r : α → α → Prop) → α → Quot r
Quot.lift: (f : α → β) → (∀ a b, r a b → f a = f b) → Quot r → β
Quot.ind : (∀ a, β (Quot.mk r a)) → ∀ q, β q

con la regla de cómputo Quot.lift f h (Quot.mk r a) ≡ f a. El axioma Quot.sound : r a b → Quot.mk r a = Quot.mk r b es lo único no computacional. Tener cocientes en el kernel evita el setoid hell que padece Coq y es una de las razones prácticas de la productividad de mathlib.

Igualdad definicional

La relación ≡ que el kernel decide incluye:

La distinción definicional (≡) vs. proposicional (=) es la fuente de la mayor parte de las dificultades prácticas. Lo que es definicionalmente igual se sustituye gratis; lo que es solo proposicionalmente igual exige rw, subst o transporte explícito, y en tipos dependientes el transporte cambia el tipo de los términos.

I.2 Los tres axiomas

El CIC puro es constructivo. Mathlib no lo es. Añade:

axiom propext : ∀ {a b : Prop}, (a ↔ b) → a = b
axiom Quot.sound : ∀ {α} {r : α → α → Prop} {a b}, r a b → Quot.mk r a = Quot.mk r b
axiom Classical.choice : ∀ {α : Sort u}, Nonempty α → α

Classical.choice + propext ⟹ tercio excluso, por el argumento de Diaconescu (mathlib lo demuestra en Classical.em). El resultado neto: lógica clásica de orden superior sobre teoría de tipos dependientes.

Auditoría: #print axioms nombre_del_teorema lista de qué axiomas depende un resultado. Un teorema que solo depende de [] es constructivo; los que dependen de Classical.choice no lo son.

Efecto colateral práctico: Classical.propDecidable da una instancia Decidable p para toda p, pero no computable. Definiciones que la usan se marcan noncomputable y no se pueden ejecutar. De ahí la tensión constante en mathlib entre generalidad y computabilidad.

I.3 Metateoría

Resultado principal (Carneiro, The Type Theory of Lean, MSc, CMU 2019; formalizado parcialmente en Lean4Lean):

Lean con n universos es consistente si lo es ZFC + n inaccesibles. Más precisamente: Lean es equiconsistente con ZFC + {existen n inaccesibles | n < ω}.

Construcción del modelo en ZFC: - ⟦Prop⟧ := {∅, {•}} — forzado por la irrelevancia de pruebas y la elección. - ⟦∀ x : α, β⟧ := funciones f con dominio ⟦α⟧ tales que f(x) ∈ ⟦β⟧ₓ. - ⟦Type n⟧ := V_κₙ con κₙ el n-ésimo inaccesible (universos de Grothendieck; necesarios por los tipos inductivos).

Corolario: Lean prueba Con(ZFC), luego por el segundo teorema de incompletitud ZFC ⊬ Con(Lean).

I.4 Decidibilidad del tipado

El juicio de tipado teórico es casi decidible pero no del todo. La causa es una interacción entre eliminación de subsingletons (para Acc) e irrelevancia de pruebas: decidir ≡ puede requerir decidir habitación de proposiciones.

Lean lo resuelve infraaproximando: implementa relaciones Γ ⊢ e ⇔ e' y Γ ⊩ e : α tales que

Γ ⊩ e : α  ⟹  Γ ⊢ e : α
Γ ⊢ e ⇔ e' ⟹ Γ ⊢ e ≡ e'

Es decir, el algoritmo implementado es estrictamente más restrictivo que la relación teórica: rechaza algunos términos bien tipados, nunca acepta uno mal tipado. Sound pero incompleto respecto a su propia especificación.

I.5 Base de confianza (TCB) real

Lean4Lean (Carneiro, arXiv:2403.14064) reimplementa el typechecker en Lean y avanza en verificarlo respecto a una especificación formal de la metateoría. Se señala explícitamente que probar la terminación del typechecker de Lean dentro de Lean es improbable.

I.6 Comparativa de fundaciones

Trade-off central: HOL es mucho más automatizable porque es más pobre (no hay dependencia, la traducción a FOL es casi directa), pero expresar estructuras algebraicas parametrizadas y jerarquías de tipos es incómodo. DTT es lo contrario.

II. La capa de elaboración y el diseño de mathlib

Técnicamente es donde está el trabajo real. El kernel es simple; el elaborador y las convenciones de biblioteca son lo que hace o rompe un proyecto.

II.1 Clases de tipos y jerarquía algebraica

Mathlib codifica las estructuras algebraicas como clases de tipos con herencia (extends), resueltas por búsqueda de instancias en el elaborador. Esquema:

Mul → Semigroup → Monoid → Group
Add → AddSemigroup → AddMonoid → AddGroup
                          ↘
                    Ring → CommRing → Field

Puntos técnicos:

• Estructuras bundled vs unbundled: mathlib usa clases unbundled sobre el tipo portador ([Group G], no G : GroupStructure) para álgebra, y objetos bundled (MonoidHom, Submodule) para morfismos y subobjetos. Los morfismos van bundled porque hay que hablar de ellos como elementos de un tipo.
• Duplicación aditiva/multiplicativa: Monoid/AddMonoid son jerarquías paralelas generadas con el atributo @[to_additive], que traduce automáticamente teoremas multiplicativos a aditivos.

II.2 El problema del diamante

Si C hereda de A y B, ambas de Z, la instancia Z obtenida por las dos rutas debe ser definicionalmente igual, no solo proposicionalmente. Si no lo es, dos términos que “deberían” ser el mismo no unifican y el elaborador falla con errores incomprensibles.

Soluciones estándar en mathlib, todas visibles en el código:

1. Campos redundantes con valores por defecto. Monoid incluye un campo npow : ℕ → M → M con default npowRec, y axiomas npow_zero, npow_succ. Sin ese campo, ℕ-potencia derivada de dos rutas distintas no sería defeq. Lo mismo con nsmul, zsmul, zpow.
2. SubNegMonoid incluye sub con default a + (-b), para que la resta de ℝ no dé un diamante con la resta canónica.
3. Campos de compatibilidad forzada. MetricSpace incluye su UniformSpace más un campo de prueba uniformity_dist que fuerza que la uniformidad coincida con la generada por la distancia. Sin esto, ℝ como espacio métrico y ℝ como espacio uniforme serían estructuras distintas.
4. Mixins en Prop. Las propiedades sin datos (IsDomain, NoZeroDivisors, CharZero) se declaran como clases valuadas en Prop, y por irrelevancia de pruebas nunca producen diamantes.

II.3 Filtros

Mathlib no usa ε-δ como noción primitiva de límite. Usa filtros:

def Filter.Tendsto (f : α → β) (l₁ : Filter α) (l₂ : Filter β) : Prop :=
  l₁.map f ≤ l₂

Con esto, una sola definición cubre límites de sucesiones (atTop), límites en un punto (𝓝 x), límites laterales (𝓝[>] x), límites a lo largo de un conjunto (𝓝[s] x), límites en infinito y convergencia casi por todas partes. La continuidad es:

def ContinuousAt (f : α → β) (x : α) : Prop := Tendsto f (𝓝 x) (𝓝 (f x))

Y Filter.Eventually (∀ᶠ x in l, p x) unifica “para n suficientemente grande”, “en un entorno de x”, “casi por todas partes”. El álgebra de filtros es un retículo completo, lo que permite manipular condiciones límite algebraicamente en lugar de manejar cuantificadores anidados. Es la decisión de diseño más consecuente de mathlib para análisis.

Derivada, vía o-pequeña sobre filtros:

HasFDerivAtFilter f f' x L ↔
  (fun x' => f x' - f x - f' (x' - x)) =o[L] (fun x' => x' - x)

II.4 Tipos de reales en teoría de la medida

La integral de Lebesgue no negativa (lintegral) toma valores en ℝ≥0∞ = ENNReal, un retículo completo donde ∞ es un elemento legítimo y la aritmética es total (∞ - ∞ = 0, 0 * ∞ = 0). Razones técnicas: convergencia monótona y Fatou se enuncian sin hipótesis de finitud, y los supremos existen siempre.

El coste es que hay tres tipos de reales no intercambiables: ℝ, ℝ≥0, ℝ≥0∞. Un x : ℝ≥0 no es un x : ℝ. Hay coerciones (↑), pero cada frontera exige lemas de push_cast. El proyecto Carleson documenta esto como una fuente permanente de fricción de diseño: decidir en cuál de los tres viven las constantes, los conjuntos y los integrandos.

II.5 Escala

~2,1 millones de líneas, >170.000 teoremas, >80.000 definiciones. Tiempo de compilación completa del orden de horas en máquinas grandes; el CI usa caché de .olean compilados. Cualquier refactor de la jerarquía de clases toca miles de archivos.

III. Automatización simbólica

III.1 Tácticas de decisión y semi-decisión

decide es peculiar: reduce la proposición a Bool y la evalúa en el kernel. Funciona para objetivos finitos pequeños; explota en cuanto la evaluación es costosa, porque el kernel no está optimizado para computar (aunque Lean 4 añadió aritmética GMP nativa para Nat, precisamente por esto — y ahí se introdujeron bugs).

III.2 Hammers

Arquitectura estándar en tres fases:

selección de premisas → traducción a lógica del ATP → reconstrucción de la prueba

Selección de premisas. De ~170.000 teoremas hay que elegir decenas. Métodos: k-NN sobre características sintácticas, naive Bayes, o embeddings neuronales (LeanExplore usa híbrido semántico + léxico + PageRank sobre el grafo de dependencias).

Traducción (Lean-auto). El paso difícil. Pipeline:

1. Recolección de subexpresiones maximales sin símbolos lógicos, generando teoremas ecuacionales entre ellas.
2. Monomorfización: instanciación de polimorfismo de tipos y de universos para eliminar dependencia.
3. Abstracción λ→* e instanciación de cuantificadores.
4. Salida a TPTP TH0 (Zipperposition, superposición de orden superior) o a SMT-LIB con una monomorfización adicional a FOL para Z3/cvc5, ya que los SMT no soportan HOL completo.

La corrección de la traducción está garantizada; la completitud no. Los ATP no razonan con tipos dependientes: todo lo que dependa esencialmente de ellos se pierde.

Reconstrucción. No se acepta la palabra del ATP. Lean-auto usa un checker verificado implementado en Lean; lean-smt trabaja en reconstruir pruebas SMT. La prueba reconstruida suele ser demasiado grande para leerse, por lo que se conserva la invocación de la táctica, no el término.

Alternativas sin traducción:

• Duper (Clune, Qian, Bentkamp, Avigad, ITP 2024): superposición nativa en teoría de tipos dependientes, produce términos de prueba de Lean directamente. Resuelve una clase de problemas que requieren razonamiento de orden superior genuino, inaccesibles a Metis y otros provers de primer orden.
• Canonical (2025): primer solver de habitación de tipos en DTT. Dado un tipo, busca un habitante. Sirve simultáneamente para ATP, síntesis de programas y generación de contraejemplos.

Referencia de rendimiento: el hammer de Coq resuelve ~40,8% de los teoremas de la biblioteca estándar en modo push-button con ~40 s en 8 CPU, en escenario de bootstrapping. Isabelle/Sledgehammer está por encima gracias a HOL. Lean está por debajo de ambos, y es su debilidad más citada.

IV. Cobertura de mathlib y lagunas

IV.1 Cubierto

Álgebra: jerarquía completa; teoría de Galois; álgebra homológica (complejos, funtores derivados, sucesiones espectrales parciales); álgebras de Lie; álgebras de Hopf; teoría de representaciones básica; módulos sobre anillos noetherianos, DIP, DFU.

Teoría de categorías (1-dimensional): límites y colímites, adjunciones, categorías abelianas, monoidales, haces, topologías de Grothendieck, categorías condensadas.

Topología: espacios uniformes, filtros, compactificaciones, grupos topológicos, teoría del grado parcialmente.

Análisis: cálculo de Fréchet en espacios de Banach, teoría de la medida e integración (Bochner y Lebesgue), espacios Lᵖ, análisis de Fourier, análisis complejo (Cauchy, residuos, funciones holomorfas), análisis funcional (Hahn–Banach, Banach–Steinhaus, teoría espectral básica, C*-álgebras en desarrollo).

Teoría de números: cuerpos de números, anillos de enteros, ideales fraccionarios, adeles e ideles, curvas elípticas (modelos de Weierstrass, ley de grupo), formas modulares (parcial), teorema de los números primos.

Geometría algebraica: espacios anillados localmente, esquemas, Proj (incluida la versión multigraduada), morfismos, propiedades de esquemas.

Combinatoria, probabilidad, teoría de conjuntos, computabilidad: ordinales y cardinales, forcing, determinación de Borel, máquinas de Turing, complejidad básica, movimiento browniano y cálculo estocástico en desarrollo.

IV.2 Lagunas y su causa técnica

El último caso es el más instructivo sobre la naturaleza de la biblioteca: la cobertura de mathlib es irregular por razones sociológicas, no lógicas. Un trabajo de 2026 sobre redes tensoriales tuvo que sustituir Jordan por descomposición en espacios propios generalizados más una descomposición invertible/nilpotente probada a mano.

IV.3 Diagnóstico agregado

“mathlib cubre franjas amplias pero incompletas del paisaje matemático; mientras algunos dominios, como el álgebra o la teoría de categorías, están bien representados, quedan grandes lagunas en otros, como la geometría diferencial o las EDP. Como resultado, la mayor parte de la investigación matemática actual no puede formalizarse en Lean sin un trabajo preparatorio prohibitivamente costoso.” — Formalizing Mathematics at Scale, arXiv:2605.29955

V. Proyectos de referencia

Detalles técnicos notables

Carleson. El teorema generalizado depende de siete parámetros (a, q, K, σ₁, σ₂, F, G). Se agrupan en una clase [ProofData a q K σ₁ σ₂ F G] donde todos son outParam asociados unívocamente al espacio X, de modo que nunca hay que darlos explícitamente. Los 30 folios de la prueba informal se descompusieron en un blueprint de 11 secciones: enunciado, 6 proposiciones auxiliares, la reducción, y las pruebas de cada proposición. Diseñado para que un no experto pueda formalizar un lema aislado.

Equational Theories. Detalle importante: no se formalizan los 22 millones de implicaciones. El tiempo de compilación sería prohibitivo. Se formaliza un conjunto de generadores; el resto se deduce por transitividad y dualidad fuera de Lean. Está previsto refactorizar para obtener un teorema end-to-end, pero no es prioritario.

FLT. La estrategia no es formalizar Wiles/Taylor–Wiles sino una prueba moderna, precisamente porque el objetivo declarado incluye dotar a mathlib de: formas y representaciones automorfas, representaciones de Galois, teoremas de modularity lifting, aritmética de variedades, teoría de cuerpos de clases, teoremas de dualidad aritmética y variedades de Shimura. La formalización del vocabulario es el grueso del trabajo.

VI. Sistemas de IA

VI.1 Arquitecturas

Step-level. El modelo propone una táctica; Lean devuelve el nuevo estado del objetivo; búsqueda en árbol (MCTS o best-first) sobre el espacio de estados. Ventaja: retroalimentación densa. Coste: una llamada al compilador por paso. Sistemas: AlphaProof, BFS-Prover.

Whole-proof. El modelo emite la prueba entera; se compila; el mensaje de error del compilador realimenta una nueva iteración. Ventaja: menos llamadas, aprovecha el chain-of-thought largo. Coste: señal más escasa. Sistemas: DeepSeek-Prover-V2, Kimina-Prover, Goedel-Prover-V2.

Agéntico. Bucles multi-turno con herramientas. AlphaProof Nexus (2026): subagentes prover basados en LLM que refinan sketches de prueba con sorry, pueden invocar AlphaProof como herramienta sobre subobjetivos, y un validador comprueba que el enunciado no se haya alterado y que la prueba compile sin sorry. Población de sketches con selección P-UCB, marco evolutivo opcional.

Entrenamiento. El patrón dominante es expert iteration: generar intentos, quedarse con los verificados por Lean, reentrenar. AlphaProof añade test-time RL: ante un problema difícil genera millones de variantes del propio problema y entrena sobre ellas en tiempo de inferencia. DeepSeek-Prover-V2 usa currículo por subobjetivos y arranque en frío con datos sintéticos.

Infraestructura. El cuello de botella es la verificación. Kimina Lean Server proporciona verificación REST paralelizada y extracción de tácticas para pipelines de RL a gran escala.

VI.2 Resultados

IMO 2024: AlphaProof resolvió 3 de 5 problemas formalizables, puntuación equivalente a medalla de plata. IMO 2025: Aristotle y Seed-Prover alcanzaron equivalente de oro.

Coste. El “impuesto formal” es real: DeepSeek-Math-V2 alcanzó puntuaciones casi perfectas en Putnam 2024 en lenguaje natural, mientras AlphaProof resolvía el 56% del PutnamBench completo —en promedio más fácil— consumiendo recursos masivos.

Régimen de investigación. DeepMind hizo un barrido sobre problemas de Erdős; de 200 soluciones candidatas marcadas como correctas o incorrectas, solo el 6,5% eran “significativamente correctas”. Cuatro problemas de Erdős fueron resueltos autónomamente en diciembre de 2025. LeanMarathon (2026) formalizó siete teoremas objetivo de dos artículos recientes de teoría de números analítica sobre problemas de Erdős, con 258 lemas descargados y sin sorry.

VI.3 Autoformalización: el cuello de botella medido

Verificar una prueba tiene oráculo (el compilador). Verificar que un enunciado formal corresponde al informal, no.

Datos:

• 19% de las formalizaciones producidas por un autoformalizador puntero sobre análisis de posgrado presentan al menos un fallo de fidelidad: hipótesis debilitada, cuantificador invertido, objetivo trivializado (The Faithfulness Gap, arXiv:2606.16541).
• Los benchmarks estándar (miniF2F, ProofNet, LeanDojo) miden capacidad de demostración condicionada a que el enunciado sea correcto; el error de arriba les es invisible.
• Revisión de miniF2F (arXiv:2511.03108): los enunciados formales del benchmark están significativamente simplificados respecto a los informales. Con traducciones más fieles, los teoremas se vuelven más difíciles y las tasas caen. La precisión reportada en la literatura suele estar evaluada por LLM, no por humanos familiarizados con Lean.
• Lean-GAP (Dummit & Foote formalizado): “cuando un autoformalizador no entiende la matemática detrás del enunciado, tiende a copiar las palabras en lugar de producir una formalización fiel, incluso cuando el problema parece rutinario y los ingredientes ya están en Mathlib”. Caso documentado: una formalización que compilaba pero no codificaba ni la propiedad definitoria de un anillo de valuación discreta ni la estructura correcta de cuantificadores.

Mitigaciones actuales: métricas de equivalencia neuro-simbólicas (BEq, equivalencia definicional bidireccional extendida), jueces de fidelidad en lenguaje natural, generación de repertorios diversos de formalizaciones para cubrirse frente a la sensibilidad del prover al fraseo del enunciado. Ninguna es un oráculo.

VI.4 Autoformalización a escala

Formalizing Mathematics at Scale (arXiv:2605.29955): un agente autoformalizador aplicado a 26 libros de texto de acceso abierto —análisis real, complejo, funcional, Fourier, diferencial; álgebra abstracta y teoría de Lie; geometría algebraica y diferencial; topología algebraica; teoría de números; combinatoria; EDP; probabilidad; informática teórica—, con intervención humana entre nula y unos mensajes al día, ~1 semana por libro. Resultado: >45.000 declaraciones de Lean 4 verificadas.

La lectura correcta: la anchura se está automatizando rápido (rellenar el sustrato de licenciatura y posgrado temprano). La profundidad no: FLT sigue con horizonte 2029, financiación dedicada y decenas de expertos.

VI.5 Factor de de Bruijn

Cociente entre tamaño de la prueba formal y de la informal. Estimaciones en Isabelle para resultados de teoría de números: 13 a 25, con los valores altos donde hubo que rellenar argumentos intermedios no explicitados en el original (por ejemplo, Erdős–Straus).

Buzzard, en el blueprint de FLT, sobre dónde se va el tiempo: el ordenador exige todos los detalles técnicos y no acepta apelaciones a la autoridad; y solo empieza a rellenar detalles por sí mismo cuando los argumentos son absolutamente obvios. La zona intermedia —rutinaria para un experto pero no trivial— absorbe el esfuerzo.

VII. Bibliografía

Fundamentos y metateoría

• Carneiro, M. (2019). The Type Theory of Lean. MSc thesis, CMU. — https://github.com/digama0/lean-type-theory
• Carneiro, M. (2024). Lean4Lean: Towards a formalized metatheory for the Lean theorem prover. arXiv:2403.14064.
• de Moura, L. & Ullrich, S. (2021). The Lean 4 Theorem Prover and Programming Language. CADE-28.
• Ebner, G., Ullrich, S., Roesch, J., Avigad, J. & de Moura, L. (2017). A metaprogramming framework for formal verification. Proc. ACM Program. Lang. 1 (ICFP).
• Werner, B. (1997). Sets in types, types in sets. TACS’97.
• Coquand, T. & Huet, G. (1988). The Calculus of Constructions. Information and Computation 76.
• Avigad, J., de Moura, L., Kong, S. & Ullrich, S. Theorem Proving in Lean 4. — https://leanprover.github.io/theorem_proving_in_lean4/
• Palmgren, E. (2017). On equality of objects in categories in constructive type theory. arXiv:1708.01924.

Diseño de mathlib

• The mathlib Community (2020). The Lean mathematical library. CPP 2020.
• van Doorn, F., von Raumer, J. & Buchholz, U. Homotopy type theory in Lean [clases de tipos y jerarquías].
• Avigad, J., Commelin, J., Macbeth, H. & Topaz, A. (2025). Anatomy of a formal proof. Notices AMS 72:2, 188–195.
• Lean community, Mathlib naming conventions y Pitfalls. — https://leanprover-community.github.io/extras/pitfalls.html
• Bordg, A. & Cavalleri, N. (2021). Elements of Differential Geometry in Lean: A Report for Mathematicians. arXiv:2108.00484. [Tratamiento de la igualdad en Lean vs. práctica informal]
• Wieser, E. & Song, U. (2022). Formalizing Geometric Algebra in Lean. Adv. Appl. Clifford Algebras.

Automatización

• Qian, Y., Song, X., Clune, J., Bentkamp, A. & Avigad, J. (2025). Lean-auto: An Interface between Lean 4 and Automated Theorem Provers. arXiv:2505.14929.
• Clune, J., Qian, Y., Bentkamp, A. & Avigad, J. (2024). Duper: A Proof-Producing Superposition Theorem Prover for Dependent Type Theory. ITP 2024, LIPIcs 309.
• Canonical for Automated Theorem Proving in Lean (2025). arXiv:2504.06239.
• Czajka, Ł. & Kaliszyk, C. (2018). Hammer for Coq: Automation for Dependent Type Theory. J. Automated Reasoning 61.
• Limperg, J. & From, A.H. (2023). Aesop: White-Box Best-First Proof Search for Lean. CPP 2023.
• Asher, J. (2025). LeanExplore [búsqueda híbrida semántica/léxica/PageRank sobre mathlib y otros paquetes].
• Santos, M. et al. (2025). Kimina Lean Server. arXiv:2504.21230.

Proyectos de formalización

• Commelin, J. et al. (2022). Completion of the Liquid Tensor Experiment. — https://leanprover-community.github.io/blog/posts/lte-final/
• Tao, T., Dillies, Y. & Mehta, B. (2023). Formalization of the Polynomial Freiman–Ruzsa conjecture of Marton. — https://github.com/teorth/pfr
• Becker, L., van Doorn, F., Jamneshan, A., Srivastava, R. & Thiele, C. (2024). Carleson operators on doubling metric measure spaces [blueprint]. arXiv:2405.06423.
• van Doorn, F. et al. (2026). Formalization of Carleson’s theorem in Lean. — https://florisvandoorn.com/carleson/paper.pdf
• Massot, P., Nash, O. & van Doorn, F. Sphere eversion project. — https://leanprover-community.github.io/sphere-eversion/
• Buzzard, K. & Taylor, R. (2026). Towards a Lean proof of Fermat’s Last Theorem [blueprint]. — https://imperialcollegelondon.github.io/FLT/blueprint.pdf
• Han, J.M. & van Doorn, F. (2020). A Formalization of Forcing and the Unprovability of the Continuum Hypothesis. ITP 2020.
• Tao, T. et al. (2025). The Equational Theories Project. arXiv:2512.07087.
• Dahmen, S.R., Hölzl, J. & Lewis, R.Y. (2019). Formalizing the Solution to the Cap Set Problem. arXiv:1907.01449.
• A formalization of Borel determinacy in Lean (2025). arXiv:2502.03432.
• A Formalization of the Mean-Field Derivation of the Vlasov Equation (2026). arXiv:2607.08986.
• Multi-agent Autoformalization of Tensor Network Theory (2026). arXiv:2607.07857. [Inventario de lagunas de mathlib]
• Mayeux, A. et al. (2025). The multi-graded Proj construction in Lean. arXiv:2509.xxxxx.

IA para demostración

• Google DeepMind (2025). Olympiad-level formal mathematical reasoning with reinforcement learning [AlphaProof]. Nature. — https://www.nature.com/articles/s41586-025-09833-y
• Tsoukalas, G. et al. (2026). Advancing Mathematics Research with AI-Driven Formal Proof Search [AlphaProof Nexus]. arXiv:2605.22763.
• Ren, Z.Z. et al. (2025). DeepSeek-Prover-V2. arXiv:2504.21801.
• Xin, H. et al. (2025). DeepSeek-Prover-V1.5: Harnessing proof assistant feedback for RL and MCTS. ICLR 2025.
• Chen, L. et al. (2025). Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving. arXiv:2507.23726.
• ByteDance (2025). Seed-Prover 1.5. arXiv:2512.17260.
• Lin, Y. et al. (2025). Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction. arXiv:2508.03613.
• Xin, R. et al. (2025). BFS-Prover: Scalable best-first tree search for LLM-based ATP. arXiv:2502.03438.
• Trinh, T.H. et al. (2024). Solving Olympiad Geometry without Human Demonstrations [AlphaGeometry]. Nature.
• Feng, T. et al. (2026). Semi-autonomous mathematics discovery with Gemini: A case study on the Erdős problems. arXiv:2601.22401.
• Formalizing Mathematics at Scale (2026). arXiv:2605.29955.
• LeanMarathon: Toward Reliable AI Co-Mathematicians through Long-Horizon Lean Autoformalization (2026). arXiv:2606.05400.
• Lean Atlas: An Integrated Proof Environment for Scalable Human–AI Collaborative Formalization (2026). arXiv:2604.16347.
• Polu, S. & Sutskever, I. (2020). Generative Language Modeling for Automated Theorem Proving. arXiv:2009.03393. [Origen del expert iteration]

Autoformalización y benchmarks

• Zheng, K., Han, J.M. & Polu, S. (2022). MiniF2F. ICLR.
• Azerbayev, Z. et al. (2023). ProofNet. arXiv:2302.12433.
• Yang, K. et al. (2023). LeanDojo. NeurIPS.
• Tsoukalas, G. et al. (2024). PutnamBench. NeurIPS.
• Glazer, E. et al. (2024). FrontierMath. arXiv:2411.04872. — https://epoch.ai/frontiermath
• Jiang, X. et al. (2025). FATE: A Formal Benchmark Series for Frontier Algebra. arXiv:2511.02872.
• Formal Conjectures: An Open and Evolving Benchmark for Verified Discovery in Mathematics (2026). arXiv:2605.13171.
• The Faithfulness Gap: Certifying Semantic Equivalence Between Informal and Formal Statements (2026). arXiv:2606.16541.
• Lee, S. et al. (2026). Lean-GAP: A Dataset of Formalized Graduate Algebra Problems. arXiv:2606.02588.
• miniF2F-Lean Revisited: Reviewing Limitations and Charting a Path Forward (2025). arXiv:2511.03108.
• Faults in Our Formal Benchmarking (2026). arXiv:2606.29493.
• Beyond the Library: An Agentic Framework for Autoformalizing Research Mathematics (2026). arXiv:2606.31134.
• Liu, Q. et al. (2025). BEq: towards a faithful metric and a dependency retrieval for statement autoformalization. ICLR 2025.
• AI for Mathematics: Progress, Challenges, and Prospects (2026). arXiv:2601.13209.

Metodología de formalización

• Avigad, J. & Harrison, J. (2014). Formally verified mathematics. Comm. ACM 57:4, 66–75.
• Avigad, J. (2024). Automated reasoning for mathematics. En Automated Reasoning, Part I, LNCS/LNAI 14739, Springer, 3–20.
• Wiedijk, F. The de Bruijn factor. — https://www.cs.ru.nl/~freek/factor/
• Massot, P. leanblueprint. — https://github.com/PatrickMassot/leanblueprint
• Notices of the AMS (2008). Special Issue on Formal Proof [Hales, Gonthier, Harrison, Wiedijk].

Recursos

• Lean community. — https://leanprover-community.github.io/
• Zulip de Lean. — https://leanprover.zulipchat.com/
• Xena Project (Buzzard). — https://xenaproject.wordpress.com/
• Blog de Tao, etiqueta Equational Theory Project. — https://terrytao.wordpress.com/tag/equational-theory-project/

Las secciones I–IV son estables. Las secciones V–VI (benchmarks y sistemas de IA) envejecen en meses.