mathlas: búsqueda y cotejo matemáticos sin API key — busca primero teoremas existentes

Para quién

Haces matemáticas en Claude Code o Cursor y quieres que el modelo invente menos teoremas, constantes y sucesiones, sin pedir otro API key. mathlas no ejecuta un modelo grande, no pide key y es gratis. Da candidatos, veredictos, inventarios y andamiaje; el razonamiento lo sigue haciendo tu AI.

Encaja en dos tareas concretas: recuperar teoremas reales con search_existing_math en un índice de unos 3,68 millones de artículos; o identificar una constante desconocida con identify_constant (PSLQ más emparejamiento de forma cerrada, 50 dígitos) y una sucesión de enteros con identify_sequence (emparejamiento exacto de términos OEIS).

Repositorio oficial en su propia línea:

https://github.com/Archerkattri/mathlas

Primer intento en 3 minutos

Solo esta línea oficial de conexión. Primero hace falta uv. Documentación de uv en su propia línea:

https://docs.astral.sh/uv/

Luego ejecuta:

claude mcp add mathlas -- uvx mathlas-mcp

Requisito: uv instalado. No hace falta API key. El texto oficial dice nothing to install first, pero sigue dependiendo de uv.

Dónde configurar: Claude Code usa la línea add de arriba; Cursor u otro cliente MCP apunta stdio a la misma uvx mathlas-mcp. No abras a la vez python -m mathlas.server como vía principal. El servicio prefiere el mcp SDK oficial y, si falta, cae a stdio JSON-RPC sin dependencias; oficialmente siempre arranca.

Primer paso de bajo riesgo: llama a search_existing_math y busca un teorema existente en el índice de 3.68M documentos. Es recuperación: devuelve datos para que razone el modelo y no cambia tu repositorio. La señal de éxito son candidatos o aciertos, no una prueba nueva. Hay doce herramientas; esta página nombra solo algunas — no inventes el resto.

No leas «sin LLM, sin API key» como sin red o sin lecturas locales. uvx levanta un proceso local; búsqueda y verificación pueden leer datos locales opcionales. Aunque aparezca readOnlyHint, no es riesgo cero.

Casos de uso

Caso 1: cotejar primero un teorema que podría ser alucinación. Llama a search_existing_math y busca un teorema real en el índice 3.68M. El texto oficial también menciona verify_numeric y verify_formal para comprobar aserciones, y habla de riesgo de alucinación cero; verify_formal necesita una cadena Lean y, si falta, devuelve con claridad data/toolchain not available en vez de fabricar una respuesta. Esta página no tiene su tabla de parámetros.

Caso 2: reconocer una constante o una sucesión de enteros. Llama a identify_constant con PSLQ más emparejamiento de forma cerrada, precisión de 50 dígitos. O identify_sequence para un emparejamiento exacto de términos OEIS. identify_sequence necesita una copia local de OEIS; si falta, degrada con honestidad y devuelve no disponible en vez de un acierto falso. El texto oficial no da un ejemplo de formato de entrada.

Límites de uso

No hace falta API key, pero sí uv. De las doce herramientas esta página solo nombra search_existing_math, verify_numeric, verify_formal, identify_constant, identify_sequence. Si faltan Lean o OEIS local, las herramientas dicen que no están disponibles y no inventan. mathlas solo devuelve datos; la prueba la termina el modelo. Sin datos locales opcionales, las funciones se contraen. El texto oficial no describe frecuencia de actualización del índice, uso de recursos ni deshacer. No leas «riesgo de alucinación cero» como si las herramientas de verificación nunca tocaran esta máquina.