Sua IA pode parar de alucinar matemática: um núcleo Lean real sobre MCP

Eu fiquei cansado de ver assistentes de IA citando teoremas de forma confiante e errada, então eu construí mathlas: um servidor MCP que fornece a qualquer agente um verdadeiro núcleo Lean, PSLQ, correspondência OEIS e um índice de teoremas com 3,68 milhões de documentos. Sem LLM por dentro, sem chave de API, Apache-2.0.

A premissa é uma divisão estrita de trabalho: a IA é o cérebro, mathlas são as mãos. Cada ferramenta retorna dados — candidatos, veredictos, listas de verificação — e o agente faz o julgamento. Nenhuma ferramenta dentro do mathlas chama uma LLM, o que significa que nenhuma ferramenta dentro do mathlas pode alucinar.

A disciplina: à prova de falhas ou nada

Cada nível que produz veredictos segue uma regra: retornar um fato verificável de forma independente, ou um honesto "nada". Nunca um palpite plausível.

Veja como isso se parece na prática — saídas reais de ferramentas em processo, capturadas do servidor ao vivo:

verify_formal executa o verdadeiro núcleo Lean 4.31.0. Dê a ele uma proposição e sua prova Lean 4 e você receberá um dos seguintes:

• VERIFIED_PROOF — o núcleo verificou a declaração completa;
• REFUTED — com a mensagem de erro do núcleo verbatim, para que o agente possa corrigir e tentar novamente;
• REJECTED — por buracos sorry/admit (o Lean em si sai 0 em uma prova com desculpa; o mathlas escaneia a fonte e os diagnósticos sorryAx do núcleo, então você não pode passar um buraco despercebido);
• UNDETERMINED — quando a cadeia de ferramentas está faltando, uma importação não pode ser resolvida, ou o limite de 60 s é atingido. Um honesto encolher de ombros, nunca um veredicto falso.

No lado numérico, identify_constant e verify_numeric usam PSLQ mais uma reavaliação independente de alta precisão (50–51 dígitos). Digite 1.6449340668482264... e ele devolve pi**2/6, re-verificado — ou nada. A taxa de falsos positivos medida em todos os níveis (numérico, sequência, relações no estilo Ramanujan): zero. Entradas sem estrutura produzem zero acertos falsos, 8 em 8 vezes que tentamos provocá-lo. Tabelas completas com comandos de reprodução estão ao vivo em RESULTS.md.

Doze ferramentas, um pipeline

As ferramentas se compõem em um fluxo de trabalho que o agente conduz:

search_existing_math → applicability_checklist / mapping_scaffold → (AI judges) → verify_numeric / verify_formal

O lado de recuperação é search_existing_math, servido de um índice denso de 3.683.428 documentos + BM25 + RRF (o lado de texto está aberto no Hugging Face). applicability_checklist é a ferramenta da qual mais me orgulho e a que ninguém mais oferece: ela decompõe as hipóteses de um teorema em pré-condições atômicas que a IA verifica uma a uma — a proteção contra a aplicação do teorema do ponto fixo de Banach a um espaço incompleto. Depois há identify_sequence (correspondência exata de termos OEIS), search_formal_math (proxies Loogle + LeanSearch para declarações mathlib, rotuladas por proveniência), conjecture_relation (PSLQ no estilo da Máquina de Ramanujan sobre uma base rica), um ambiente sandboxed funsearch, e add_finding, que é importante para o benchmark abaixo.

O benchmark, com sua ressalva à frente

Nos próprios 110 questionários escritos por humanos do TheoremSearch, o mathlas com seu loop de auto-augmentação na web pontua 59,1% de Hit@20 a nível de teorema (65/110) contra 45,0% do TheoremSearch. Parece ótimo. Aqui está a parte que você deve ler antes de citá-lo:

Esta é uma comparação de loop-vs-estático, não de corpus-vs-corpus. Apenas corpus, a linha de base do mathlas neste benchmark é 10,0% — o TheoremSearch reteve ~85% de seu corpus privado de 9,2 milhões (os artigos licenciados pelo arXiv que não podem ser redistribuídos), então 95 dos 110 artigos-alvo são inacessíveis para qualquer sistema aberto. O que os 59,1% medem é o loop add_finding: o agente encontra na web cada declaração faltante, a incorpora com o mesmo Qwen3-Embedding-8B e a funde no índice ao vivo em tempo real. Os 45,0% do TheoremSearch são um sistema estático respondendo de seu corpus privado completo. A manchete honesta é "um loop de gravação validado repara a lacuna de cobertura de um sistema aberto em tempo real", não "meu índice supera o deles". O domínio matemático é o lugar certo para tal loop precisamente porque o candidato de gravação pode ser verificado de forma determinística (verify_numeric / verify_formal) antes de ser confiável.

Reproduza-o com benchmarks/webaug_110_bench.py no repositório.

Experimente em uma linha

Com uv instalado:

claude mcp add mathlas -- uvx mathlas-mcp

É isso — Claude Code agora vê doze ferramentas. O pip simples também funciona (pip install mathlas-mcp), o Cursor ou qualquer cliente MCP pode apontar para o mesmo comando stdio, e se o SDK oficial mcp não estiver instalado, o servidor recua para uma implementação JSON-RPC stdio sem dependências, então sempre funciona. Também está no registro oficial do MCP como io.github.Archerkattri/mathlas.

O que ele não faz

mathlas não escreve provas — a divisão entre gerador/verificador é absoluta, então o núcleo verifica sua prova e relata exatamente por que ela falha, mas a correção fica por sua conta (ou de seu agente). A recuperação apenas de corpus não superará o TheoremSearch em seu benchmark; a linha de base de 10,0% é um piso limitado por licenciamento e eu a reporto como tal. Duas ferramentas se degradam sem dados locais opcionais: identify_sequence quer uma cópia local do OEIS e verify_formal quer uma cadeia de ferramentas Lean — sem elas você recebe um claro "não disponível", nunca uma resposta falsa. O índice de qualidade total precisa do codificador Qwen3-Embedding-8B, que não é hardware de laptop; existem níveis quantizados e de 0,6B medidos que trocam 7–9 pontos de recall para rodar em 4 threads de CPU, documentados com seus custos exatos. E não é um CAS — se você