mathlas

mathlas

Disponible en mcp.so · Glama · listado en awesome-mcp-servers y best-of-lean4.

Una herramienta matemática a prueba de filtraciones que una IA usa — sin LLM, sin clave API, gratis. Conéctala a Claude Code, Cursor o cualquier cliente MCP. La IA es el cerebro; mathlas es las manos — le da a la IA las capacidades que le faltan y devuelve datos (candidatos, veredictos, listas de verificación, andamios) para que la IA razone sobre ellos. Apache-2.0. El código es libre para cualquier uso; los artefactos publicados del corpus/índice tienen sus propios términos por fuente (CC-BY/CC0).

_{Cada veredicto proviene del kernel real de Lean 4.31.0 / PSLQ + una re-evaluación independiente — sin LLM dentro. Salidas reales de herramientas en proceso, capturadas por assets/gen/capture_outputs.py.}

---

¿Es esto para ti?

• Usas Claude Code / Cursor y quieres que tu IA deje de alucinar matemáticas — search_existing_math encuentra el teorema real desde un índice de 3.68M de documentos; verify_numeric y verify_formal verifican afirmaciones con riesgo cero de alucinación.
• Tienes una constante numérica o una secuencia de enteros que no puedes identificar — identify_constant ejecuta PSLQ + coincidencia de forma cerrada (precisión de 50 dígitos); identify_sequence hace una coincidencia exacta de términos con OEIS.
• Necesitas el nombre formal (Lean/mathlib) de un resultado — search_formal_math actúa como proxy de los servicios públicos Loogle y LeanSearch y devuelve nombres de declaraciones + tipos, etiquetados por procedencia.
• Estás construyendo un pipeline de agentes que necesita matemáticas a prueba de filtraciones en el bucle — las 12 herramientas son herramientas MCP puras que devuelven datos, sin LLM dentro, componibles con cualquier framework.

---

Instalación y registro con Claude Code (sin clave API)

Una línea, sin necesidad de instalar nada primero (requiere uv):

claude mcp add mathlas -- uvx mathlas-mcp

uvx mathlas-mcp descarga + ejecuta el servidor en un entorno aislado en el primer uso. ¿Prefieres pip?

pip install mathlas-mcp              # core: numeric + retrieval + verify + scaffolds
pip install 'mathlas-mcp[mcp]'       # + official MCP SDK
pip install 'mathlas-mcp[retrieve]'  # + pyarrow, to read the real index
pip install 'mathlas-mcp[embed]'     # + sentence-transformers/torch, for the Qwen3 embedder

claude mcp add mathlas -- python -m mathlas.server

mathlas ahora aparece como doce herramientas que el agente puede llamar. El servidor prefiere el SDK oficial mcp y cae a un servidor JSON-RPC stdio sin dependencias si mcp no está instalado — siempre se ejecuta. (Cursor / cualquier cliente MCP: apúntalo al mismo comando stdio uvx mathlas-mcp o python -m mathlas.server.)

Datos locales opcionales (degradación honesta): identify_sequence quiere una copia local de OEIS; verify_formal quiere un toolchain de Lean. Sin ellos, las herramientas devuelven un claro "datos/toolchain no disponibles" — nunca una respuesta falsa. Consulta docs/methods.md para la configuración de una línea de cada uno.

---

Un ejemplo práctico — una IA usando las herramientas

User:  "Does x = cos(x) have a unique solution I can reach by iterating?"

AI →   search_existing_math("contraction mapping unique fixed point complete metric space")
       ← [{name:"Banach Fixed-Point Theorem", statement:"Let (X,d) be a complete metric
            space and T a contraction. Then T has a unique fixed point ...", ...}, ...]
AI →   applicability_checklist(banach.statement)
       ← preconditions: ["(X,d) is a complete metric space", "T: X→X is a contraction"]
          conclusion:    "T has a unique fixed point"
AI  (reasons): [0,1] is complete; cos is a contraction there (|cos'|=|sin|≤sin 1<1).
       Every precondition holds ⇒ Banach applies ⇒ unique fixed point, reachable by iteration.
AI →   verify_numeric("0.7390851332151607", "<the Dottie-number closed form, if claimed>")

mathlas proporcionó la búsqueda, la lista de verificación y la verificación numérica a prueba de filtraciones. La IA hizo el juicio. No se llamó a ningún LLM dentro de mathlas.

---

Resultados

La disciplina es a prueba de filtraciones o nada: un resultado es un hecho verificable de forma independiente o un honesto "nada." La tasa de falsos positivos es 0 en todos los niveles (tablas completas + comandos en RESULTS.md):

Nivel	Recuperación@conocidos	Falso positivo	Por qué es a prueba de filtraciones	Benchmark
Numérico (identify_constant)	8/8	0/3	re-evaluación independiente de alta precisión (50–51 dígitos)	benchmarks/numeric_bench.py
Secuencia (identify_sequence)	8/8 (7 top-1)	0/3	coincidencia exacta de términos vs OEIS local (~400k secuencias)	benchmarks/tier_bench.py
Formal (verify_formal)	7/7 veredictos	—	verificación de tipos del kernel real de Lean 4.31.0	benchmarks/tier_bench.py
Ramanujan (conjecture_relation)	6/6	0/2	PSLQ + CF, cada acierto re-verificado ≥25 dígitos	benchmarks/tier_bench.py
Foso de aplicabilidad	15/15 descomp. + 6/6 captura	—	precondiciones atómicas, trampas de mala aplicación	benchmarks/moat_bench.py
FunSearch + web-aug	14/14	—	contención en sandbox (red / tiempo de espera / memoria)	benchmarks/tools_bench.py

_{La tabla anterior, de un vistazo — 0 falsos positivos en todos los niveles (0/8 entradas sin estructura produjeron un acierto falso), 100% de recuperación en conocidos. Números: RESULTS.md §1–2b.}

Agente en el bucle, reportado honestamente (2026-06-10, Claude Fable 5): el mismo agente sin cabeza al que se le dieron 18 tareas matemáticas CON el servidor MCP mathlas en vivo como su única herramienta vs SIN herramientas puntúa 18/18 vs 15/18. El conjunto original de 10 tareas está saturado (10/10 en ambos sentidos: un modelo frontera lo aprueba solo con conocimiento paramétrico, y lo decimos claramente), así que se añadió un conjunto difícil de 8 tareas donde la verificación, no el recuerdo, es el cuello de botella: ese conjunto va 8/8 CON vs 5/8 SIN. El modelo desnudo se agota en la detección de relaciones de enteros de 50 dígitos (PSLQ) y no puede nombrar secuencias OEIS oscuras que ensombrecen los prefijos de Catalan/Fibonacci y solo divergen en profundidad. Los pases que el modelo desnudo logra son notables y los reportamos: evaluó una relación de constantes de 6 términos a 45 dígitos a mano (residual 1.475e-27, correcto), simuló el redondeo IEEE-754 bit a bit en su cabeza (con un exponente incorrecto en prosa), y probó una fórmula tipo Machin exactamente mediante enteros gaussianos, todo en contexto a 3-9x la latencia de una llamada a herramienta. Cada verdad fundamental es un cálculo determinista registrado en el banco; tabla completa y procedencia: RESULTS.md §2c. Ejecución: benchmarks/agent_bench.py.

El índice de 3.68M de documentos. search_existing_math se sirve desde un índice denso de 3,683,428 documentos (Qwen3-Embedding-8B, 4096-d): el subconjunto 1.34M permisivo CC-BY/CC0 de TheoremSearch + 2.34M documentos de matemáticas de arXiv con eslóganes incrustados de Dolma, denso + Okapi-BM25 + RRF. Recuerdo honesto del titular a escala completa de 3.68M: R@1 0.614 / R@10 0.832 consultando por el cuerpo crudo de un documento contra su entrada con eslogan incrustado — el régimen difícil de auto-recuperación de representación cruzada. (En la construcción anterior de 1.635M, el auto-recuperación más fácil de eslogan→eslogan de la misma representación fue R@1 0.977 / R@10 0.998 en su división retenida de 81,833 documentos.)

Corpus abierto en Hugging Face. El lado de texto + metadatos de ese índice se publica en kattri15/mathlas-corpus: 3,683,428 documentos a nivel de teorema más la pequeña configuración findings, divididos en configuraciones theoremsearch, dolma y findings. Incluye eslóganes, declaraciones LaTeX, URLs de origen, títulos, etiquetas, categorías, conteos de citas cuando se conocen y claves de procedencia. No incluye las matrices de incrustación de 30 GB ni las rebanadas de benchmark local. Las licencias son por configuración: subconjunto de TheoremSearch CC BY-SA 4.0, declaraciones de Dolma ODC-BY 1.0 con nuestros eslóganes CC BY 4.0, y hallazgos CC BY 4.0. Auditoría completa: docs/HF_DATASET_LICENSING.md.

from datasets import load_dataset

ts = load_dataset("kattri15/mathlas-corpus", "theoremsearch", split="train")
dolma = load_dataset("kattri15/mathlas-corpus", "dolma", split="train")

Nivel portátil cuantizado (opt-in). La matriz fp16 es de 30 GB en disco (~60 GB fp32 residentes) — bien en la máquina de construcción, no en un portátil. MATHLAS_QUANTIZED=binary (o quantized="binary" en HybridRetriever.from_index) sirve el MISMO índice desde sidecars cuantizados mapeados en memoria en su lugar: Hamming de bit de signo sobre 1.9 GB preselecciona 1000 candidatos, el re-escore exacto elige el top-k — medido en el índice completo de 3.68M con el mismo protocolo n=3000 que el titular, es sin pérdida de recuerdo (R@1 0.6143 vs 0.6140 fp16, R@10 igual en 0.8323; modo int8: R@1 0.6147, 15 GB) a 2.4 s/consulta en 4 hilos de CPU. Advertencia honesta: esto encoge solo el lado del documento — las consultas aún deben incrustarse con el mismo Qwen3-Embedding-8B (un pequeño codificador de 0.6B vive en un espacio vectorial diferente). El verdadero nivel de extremo a extremo con codificador pequeño es el nivel de 0.6B a continuación. Números, comando de construcción y la advertencia completa: docs/QUANTIZED_TIER.md.

Nivel portátil de extremo a extremo 0.6B (opt-in). El MISMO corpus de 3,683,428 documentos re-incrustado una vez con Qwen3-Embedding-0.6B (1024-d, alineado por filas con la meta servida), para que el codificador de consultas en sí se ejecute en una CPU de portátil: MATHLAS_ENCODER=0.6b (se compone con MATHLAS_QUANTIZED=binary). Medido con el protocolo idéntico de representación cruzada n=3000, consultas re-codificadas por el modelo de 0.6B: R@1 0.545 / R@10 0.745 (re-escore binario + int8; el escaneo exacto fp16 de 0.6B es 0.544 / 0.745, por lo que la cuantización es nuevamente sin pérdida dentro del nivel). El precio honesto vs el nivel de 8B (0.614 / 0.832) es de aproximadamente 7-9pp de recuerdo; la configuración de doble canal de 8B (0.965 / 0.999) sigue siendo el techo de calidad de la caja grande. El titular del portátil: 0.67 s/consulta de extremo a extremo en 4 hilos de CPU (0.88 s en 2), codificación de consultas incluida, sobre los 3.68M de documentos. Huella del canal denso: sidecar binario 0.47 GB + codificador de 0.6B ~1.2 GB (~1.7 GB; fuente de re-escore int8 3.77 GB recomendada; índice hermano fp16 completo 7.54 GB). En la sonda solo del corpus TheoremSearch-110, el nivel puntúa Hit@20 8.2% / 10.0% teorema/artículo vs el 10.0% / 11.8% del nivel de 8B (ambos pisos limitados por licencia). Tablas completas, huellas y advertencias: docs/QUANTIZED_TIER.md; construcción: scripts/build_06b_index.py; evaluación: scripts/eval_06b_tier.py.

Recuperación de doble canal (opt-in). El titular de 0.614 es una brecha de representación cruzada: consultas con forma de declaración LaTeX buscadas contra documentos con eslóganes incrustados. Un segundo canal denso incrusta los mismos 3,683,428 documentos por su declaración LaTeX limpia (Qwen3-Embedding-8B, alineado por filas, construido por scripts/build_statement_channel.py) y se pliega en la clasificación densa por max-sim por documento. Medido en la misma muestra n=3000 a escala completa del corpus: R@1 0.614 a 0.965, R@10 0.832 a 0.999. Advertencias honestas: esa evaluación es un proxy de auto-recuperación en el que el canal de declaraciones indexa el mismo texto del que se extraen las consultas (una ventaja de texto exacto, como la de BM25); en el benchmark de 110 consultas humanas sin fuga, el aumento es real pero parcial (Hit@20 de artículo 11.8% a 12.7%). Y la segunda matriz aproximadamente duplica la RAM de servicio (medida a escala completa: pico de proceso de 150 GB para el servidor dual vs ~95 GB de un solo canal; ~2.75 s/consulta de escaneo denso dual en 2 hilos de CPU), por lo que se envía estrictamente opt-in (MATHLAS_STATEMENT_INDEX=/path/index_full_statement.npz, nunca auto-detectado) y no es combinable con el nivel cuantizado. Números completos y la tabla del nivel de servicio: docs/RETRIEVAL_UPGRADE_NOTES.md. El híbrido de producción por defecto rrf_k es 10 (mejor medido en cada k probado), más una mezcla de re-clasificación con codificador cruzado opt-in (MATHLAS_RERANK=1, Qwen3-Reranker-0.6B, +1.7pp de aumento honesto de R@1). El backend de re-clasificación es seleccionable con MATHLAS_RERANK_MODEL: qwen3 (por defecto, Qwen3-Reranker-0.6B, sin cambios) o jina-v3 (jinaai/jina-reranker-v3, arXiv:2509.25085 — un re-clasificador de 0.6B "último pero no tarde" que lidera BEIR a la escala de 0.6B). Ambos cargan sus pesos de forma perezosa en el primer uso y caen a la fusión sin re-clasificar (nota honesta en stderr) si torch/transformers o los pesos están ausentes; un nombre de modelo mal escrito genera un error en lugar de servir silenciosamente el re-clasificador incorrecto. Enviamos el cableado, no un número de benchmark de jina — trae tus propios pesos.

El bucle de auto-aumento — superando a TheoremSearch

En las 110 consultas escritas por humanos de TheoremSearch, el mathlas base alcanza un piso de cobertura — TheoremSearch retuvo el 85% de su corpus privado de 9.2M, por lo que 95 artículos objetivo son inalcanzables para cualquier sistema abierto. La IA luego ejecuta el bucle: para cada teorema faltante, encuentra en la web la declaración real, la incrusta con el mismo Qwen3-Embedding-8B, y add_finding(dense_vec=…) la fusiona a través del canal denso en tiempo de ejecución (re-medido 2026-06-10 en el índice servido de 3.68M — el titular posterior al bucle se reprodujo exactamente; la línea base solo del corpus bajó 13.6% → 11.8% a nivel de artículo por los distractores añadidos de Dolma, reportado tal cual):

Método	Teorema Hit@20	Paper Hit@20
Google (site:arxiv.org)	—	37.8%
ChatGPT 5.2 con Búsqueda	19.8%	—
Gemini 3 Pro	27.0%	—
TheoremSearch (Qwen3-8B, corpus privado completo de 9.2M)	45.0%	56.8%
mathlas — línea base (solo corpus)	10.0%	11.8%
mathlas — tras el bucle web de autoaumento	59.1% (65/110)	70.0% (77/110)

_{Este es el valor del bucle, no una afirmación del corpus nativo. La línea base del 10.0% está limitada por licencias — TheoremSearch retuvo ~85% de su corpus de 9.2M, por lo que 95/110 papers objetivo son inalcanzables para cualquier sistema abierto; el bucle web de autoaumento repara esa brecha de cobertura en tiempo de ejecución de IA. La barra de Google es a nivel de paper Hit@20 (sin número de teorema reportado); todas las demás barras son a nivel de teorema Hit@20.}

Reproducir con benchmarks/webaug_110_bench.py (usar la lista de trabajo completa de 82 hallazgos _findings_worklist_full.json).

Recuperación consciente de la fuente (opt-in). Crecir el índice de 1.34M → 3.68M tuvo un costo medido: los 2.34M de documentos Dolma extraídos de la web desplazan a los papers canónicos del top-20 (nivel de paper solo corpus 13.6% → 11.8% en estas mismas 110 consultas). search_existing_math ahora acepta source_filter / source_weights opcionales — p. ej., source_filter={"exclude": ["dolma"]} cuando solo quieres declaraciones de teoremas canónicos — y excluir dolma recupera completamente el 13.6% previo al crecimiento a nivel de paper (15/110; paper alcanzable-15 15/15 = 100%) con nivel de teorema por encima del índice antiguo (11.8% vs 10.9%). El ranking predeterminado permanece byte-idéntico (fijado por pruebas). Es un interruptor por intención de consulta, no una victoria gratuita: en el auto-recall n=3000, el 65% de cuyos objetivos SÍ son documentos Dolma, reducir el peso de dolma es catastrófico para esas consultas (R@10 objetivo-dolma 0.999 → 0.884 con peso 0.5, → 0 cuando se excluye) — exactamente por eso se envía opt-in, desactivado por defecto. También probamos si el canal dual corrige esta regresión estructuralmente, sin el interruptor: recupera parte de ella (paper 11.8% a 12.7%, teorema 10.0% a 10.9% con configuraciones predeterminadas) pero no el 13.6% completo, por lo que el interruptor sigue siendo la mitigación documentada en este benchmark. Matriz completa: docs/02_eval_vs_theoremsearch.md.

---

Las 12 herramientas

search_existing_math ─▶ mapping_scaffold + applicability_checklist ─▶ (AI judges) ─▶ verify_numeric / verify_formal
   (own index)            (needs↔guarantees, no LLM)                                  (airtight)

Cuatro principales — lo que la mayoría de los agentes usan:

Herramienta	Qué hace
search_existing_math(query, k)	consulta → resultados clasificados del índice denso + BM25 + RRF de 3.68M-docs
identify_constant(value)	un valor real → forma cerrada conocida + procedencia (re-evaluación de 50 dígitos)
verify_numeric(value, closed_form)	veredicto de concordancia de dígitos — motor diferente, mayor precisión
verify_formal(statement, lean?, proof?)	ejecuta el kernel real de Lean — verifica tipos de un fragmento, o pasa proof para verificar con el kernel una prueba completa de Lean 4: VERIFIED_PROOF / REFUTED (el error exacto del kernel, para el bucle de reparación) / UNDETERMINED honesto

Kit de herramientas completo:

Herramienta	Qué hace
search_formal_math(query, backend)	nombres de declaraciones de mathlib + tipos a través de los servicios públicos Loogle (patrón/tipo) + LeanSearch (lenguaje natural), etiquetados con procedencia; "servicio no disponible" honesto — con un caché en disco de 7 días que sirve la última buena respuesta cuando un servicio está caído, claramente etiquetado (cached, <age> old)
identify_sequence(terms)	secuencia de enteros → entradas OEIS coincidentes (coincidencia exacta de términos)
applicability_checklist(statement)	hipótesis del resultado como una lista de verificación atómica para que la IA marque
mapping_scaffold(problem, statement)	preguntas de necesidades↔garantías + plantilla de relleno
conjecture_relation(value)	Ramanujan Machine: PSLQ sobre base rica + conjeturas de CF/recurrencia
funsearch(action, problem_id, …)	harness de FunSearch en una herramienta — action=evaluate (puntúa en sandbox un programa escrito por IA), register (base de datos MAP-Elites), status (mejor + few-shot)
search_directive(problem)	plan de búsqueda web: consultas arXiv + subcampos + qué herramientas ejecutar
add_finding(statement, slogan, source)	ingerir un resultado encontrado en la web en el corpus en vivo

Todas las herramientas devuelven datos. Ninguna herramienta llama a un LLM. search_formal_math es la única herramienta que hace una llamada web (a los servicios públicos Loogle/LeanSearch); todo lo demás es completamente local.

Verificación de pruebas — el bucle de reparación

verify_formal no solo verifica tipos de declaraciones: dale una proposición y tu prueba de Lean 4, y el kernel real verifica la declaración completa. mathlas nunca escribe una prueba (la división generador/verificador es absoluta) — pero cuando tu prueba es incorrecta, el kernel te dice exactamente por qué, textualmente, en kernel_error. Eso convierte la escritura de pruebas en un bucle cerrado: el agente escribe una prueba → el kernel de mathlas dice exactamente qué está mal → el agente repara y vuelve a llamar.

verify_formal(statement="∀ n : Nat, n + 0 = n", proof="by\n  intro n\n  rfl")
// → {"proof_status": "VERIFIED_PROOF", "checked": true, ...}
verify_formal(statement="2 + 2 = 5", proof="rfl")
// → {"proof_status": "REFUTED", "kernel_error": "error: Not a definitional equality:
//     the left-hand side 2 + 2 is not definitionally equal to the right-hand side 5 ...", ...}

Sin pases falsos, por construcción: los huecos sorry/admit son RECHAZADOS (el propio Lean sale con 0 en una prueba con sorries — mathlas escanea la fuente y los diagnósticos sorryAx del kernel); un toolchain faltante, un tiempo de espera (límite de 60 s), o una importación que este toolchain básico no puede resolver devuelven un UNDETERMINED honesto, nunca un veredicto. Todo el contrato está fijado por tests/test_proof_check.py (20 pruebas contra el kernel real de Lean 4.31.0: términos correctos y pruebas de bloques de tácticas verificadas, pruebas incorrectas refutadas con el mensaje del kernel, pruebas con sorries rechazadas, toolchain ausente honesto).

---

CLI / Python

mathlas 1.6449340668482264364724151666460251892   # -> pi**2/6  [verified 51 digits]
mathlas 1,1,2,3,5,8,13,21                          # -> A000045 Fibonacci  https://oeis.org/A000045
mathlas "a bounded sequence has a convergent subsequence" --k 5   # search + scaffold
mathlas mcp                                                        # run the MCP server

import mpmath
from mathlas import identify, identify_sequence, mapping_scaffold, applicability_checklist
print(identify(mpmath.zeta(2)))            # -> pi**2/6 [verified 51 digits]
print(identify_sequence([1,1,2,3,5,8,13,21]).matches[1].a_number)  # -> 'A000045'

---

Documentación

• RESULTS.md — validación de cada herramienta, reproducida, con comandos.
• docs/methods.md — arquitectura, decisiones de diseño, citas.
• docs/05_open_dataset.md — el conjunto de datos abierto y el índice.
• docs/QUANTIZED_TIER.md — el nivel de portátil cuantizado: recall/espacio/latencia medidos.
• docs/02_eval_vs_theoremsearch.md — el cara a cara de recuperación.
• docs/REGISTRY_PUBLISH.md — publicación en el registro oficial de MCP.

Posicionamiento — la recuperación es lo básico; la verificación es el foso

Crédito donde corresponde: el sistema más cercano, TheoremSearch (UW Math AI Lab), ahora envía una API REST de producción y su propio endpoint MCP (api.theoremsearch.com/mcp) sobre un corpus de 9.2M de documentos — en recall bruto sobre literatura matemática es el sistema a batir, y "somos nativos de MCP, ellos son una herramienta de laboratorio" ya no es un diferenciador. Reutilizamos solo su subconjunto de datos con licencia abierta (CC-BY/CC0) como datos brutos para nuestro propio índice — no su API, MCP, índice o código.

La señal de DeepMind, y por qué un verificador abierto aún importa. El AlphaProof Nexus de DeepMind (arXiv:2605.22763) valida precisamente la arquitectura de mathlas — un agente LLM que orquesta un kernel de Lean y recursos matemáticos estructurados como OEIS como oráculo de verdad fundamental — pero es solo interno: el artefacto público es un volcado de resultados (google-deepmind/alphaproof-nexus-results), no un sistema ejecutable, sin API y sin superficie MCP. Gemini Deep Think y sus pares solo agudizan la necesidad: a medida que los agentes razonan más, un verificador local y determinista del lado del agente que puedan llamar de forma barata y sin conexión se convierte en el cuello de botella, no el modelo. mathlas sigue siendo la única capa de verificación abierta, sin clave de API, componible con MCP que cualquier agente puede integrar hoy — y ahora también ingiere el corpus de Lean formal-conjectures de DeepMind con licencia abierta (arXiv:2605.13171) como fuente del índice (scripts/fetch_formal_conjectures.py, 3,941 declaraciones de conjeturas de Lean, etiqueta de fuente formal_conjectures, incluidos los subconjuntos de evaluación congelados FC100SolvedSet1/FC100OpenSet1).

Nota de nomenclatura: mathlas no está relacionado con Matlas (matlas.ai, búsqueda de teoremas de la Universidad de Pekín, arXiv:2604.17484) — proyecto diferente, autores diferentes; la casi homofonía es coincidencia.

Lo que ningún competidor tiene es todo lo que sucede después de la recuperación:

• Niveles de verificación — verify_numeric (re-evaluación independiente de 50 dígitos) y verify_formal (una verificación de tipos con un kernel real de Lean — incluida la verificación completa de pruebas con el error del kernel devuelto textualmente para bucles de reparación de agentes — o un UNDETERMINED honesto). La recuperación te da un candidato; mathlas también puede verificar la afirmación y verificar tu prueba de ella.
• applicability_checklist — descompone un teorema candidato en precondiciones atómicas que la IA verifica una por una, detectando aplicaciones incorrectas (intervalo abierto vs cerrado, grupo infinito vs finito). Ningún competidor tiene uno.
• El bucle de autoaumento add_finding — la IA encuentra en la web una declaración faltante, la incrusta y la fusiona en el índice en vivo en tiempo de ejecución: 59.1% vs el 45.0% de TheoremSearch en Hit@20 de teoremas en su propio benchmark de 110 consultas (ver arriba). Esto es, hasta donde sabemos, la primera instanciación en el dominio matemático de un bucle RAG de escritura validada — la familia de sistemas de recuperación bidireccional que escriben inferencia verificada de vuelta en el almacén recuperable (RAG Bidireccional, arXiv:2512.22199), en lugar de tratar la recuperación como solo lectura (Self-RAG, arXiv:2310.11511; CRAG, arXiv:2401.15884). Lo que hace que el dominio matemático sea el lugar adecuado para esto: el candidato de escritura puede ser verificado determinísticamente (verify_numeric / verify_formal) antes de ser confiado, por lo que el bucle crece el corpus sin el riesgo de amplificación de alucinaciones que conlleva un bucle de escritura genérico.
• Disciplina de cero falsos positivos — cada nivel devuelve un hecho verificable de forma independiente o un "nada" honesto; la tasa de falsos positivos medida es 0 en todos los niveles (RESULTS.md).
• Gratis, sin clave de API, etiquetado con procedencia — cada resultado lleva de dónde vino (known_constant, conjectured_relation, web_added, external:loogle, …), y el índice está construido 100% a partir de datos con licencia abierta.

	mathlas	TheoremSearch	LeanSearch / Loogle	Wolfram MCP	sympy-mcp
Recuperación matemática informal	✅ 3.68M docs, abierto	✅ 9.2M docs (~85% privado)	❌ (solo declaraciones mathlib)	❌	❌
Búsqueda formal (mathlib)	✅ proxy de ambos → una herramienta MCP	❌	✅ (es exactamente esto)	❌	❌
Verificación numérica	✅ re-evaluación hermética de 50 dígitos	❌	❌	⚠️ evaluación CAS	⚠️ CAS (sin marco de verificación de afirmaciones)
Verificación formal	✅ kernel real de Lean (declaraciones y pruebas completas, errores de bucle de reparación)	❌	❌ (búsqueda, no verificación)	❌	❌
Lista de verificación de aplicabilidad	✅ único	❌	❌	❌	❌
Corpus de autoaumento	✅ add_finding (59.1 vs 45.0 Hit@20)	❌	❌	❌	❌
Identificación de constantes/secuencias	✅ PSLQ + OEIS + Ramanujan-Machine	❌	❌	⚠️ algunas	❌
Etiquetas de procedencia	✅ cada resultado	❌	n/a	❌	n/a
Costo / clave	gratis, sin clave	endpoint gratuito	gratis	clave de API de Wolfram de pago	gratis
MCP	✅ stdio, uvx one-liner	✅ endpoint remoto	❌ (mathlas los proxya)	✅	✅

(sympy-mcp es un servidor de manipulación CAS fino — su alcance apenas se superpone: reescribe expresiones que le das; mathlas encuentra, delimita y verifica matemáticas existentes.)

---

Registro oficial de MCP

mathlas está publicado como io.github.Archerkattri/mathlas (ver docs/REGISTRY_PUBLISH.md y server.json).

mcp-name: io.github.Archerkattri/mathlas