mathlas
Matemática hermética para agentes de IA: busca de 3,7 milhões de teoremas, identificação de constantes PSLQ, OEIS, verificações reais do kernel Lean 4. Sem LLM interno, sem chave de API.
Documentação
mathlas
Disponível em mcp.so · Glama · listado em awesome-mcp-servers e best-of-lean4.
Uma ferramenta de matemática à prova de falhas que uma IA usa — sem LLM, sem chave de API, grátis. Conecte-a ao Claude Code, Cursor ou qualquer cliente MCP. A IA é o cérebro; a mathlas é as mãos — ela dá à IA as capacidades que faltam e retorna dados (candidatos, veredictos, listas de verificação, esqueletos) para a IA raciocinar. Apache-2.0. O código é livre para qualquer uso; artefatos publicados de corpus/índice têm seus próprios termos por fonte (CC-BY/CC0).
Cada veredicto vem do kernel real Lean 4.31.0 / PSLQ + uma reavaliação independente — nenhum LLM internamente. Saídas reais de ferramentas em processo, capturadas por assets/gen/capture_outputs.py.
Isto é para você?
- Você usa Claude Code / Cursor e quer que sua IA pare de alucinar matemática —
search_existing_mathencontra o teorema real em um índice de 3,68 milhões de documentos;verify_numericeverify_formalverificam afirmações com risco zero de alucinação. - Você tem uma constante numérica ou sequência de inteiros que não consegue identificar —
identify_constantexecuta PSLQ + correspondência de forma fechada (precisão de 50 dígitos);identify_sequencefaz uma correspondência exata de termos no OEIS. - Você precisa do nome formal (Lean/mathlib) de um resultado —
search_formal_mathfaz proxy dos serviços públicos Loogle e LeanSearch e retorna nomes de declarações + tipos, com rótulo de proveniência. - Você está construindo um pipeline de agente que precisa de matemática à prova de falhas no ciclo — todas as 12 ferramentas são ferramentas MCP puras que retornam dados, sem LLM interno, componíveis com qualquer framework.
Instalação e registro no Claude Code (sem chave de API)
Uma linha, nada para instalar antes (precisa de uv):
claude mcp add mathlas -- uvx mathlas-mcp
uvx mathlas-mcp busca e executa o servidor em um ambiente isolado no primeiro uso. Prefere 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
a mathlas agora aparece como doze ferramentas que o agente pode chamar. O servidor prefere o SDK oficial mcp e recai em um servidor JSON-RPC stdio sem dependências se mcp não estiver instalado — ele sempre executa. (Cursor / qualquer cliente MCP: aponte-o para o mesmo comando stdio uvx mathlas-mcp ou python -m mathlas.server.)
Dados locais opcionais (degradam honestamente):
identify_sequencequer uma cópia local do OEIS;verify_formalquer um toolchain Lean. Sem eles, as ferramentas retornam um claro "dados/toolchain não disponíveis" — nunca uma resposta falsa. Vejadocs/methods.mdpara a configuração de uma linha de cada um.
Um exemplo prático — uma IA usando as ferramentas
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>")
a mathlas forneceu a busca, a lista de verificação e a verificação numérica à prova de falhas. A IA fez o julgamento. Nenhum LLM foi chamado dentro da mathlas.
Resultados
A disciplina é tudo-ou-nada: um resultado é um fato verificável independentemente ou um honesto "nada." A taxa de falsos positivos é 0 em todos os níveis (tabelas completas + comandos em RESULTS.md):
| Nível | Recuperação@conhecido | Falso-positivo | Por que é à prova de falhas | Benchmark |
|---|---|---|---|---|
Numérico (identify_constant) | 8/8 | 0/3 | reavaliação independente de alta precisão (50–51 dígitos) | benchmarks/numeric_bench.py |
Sequência (identify_sequence) | 8/8 (7 top-1) | 0/3 | correspondência exata de termos vs OEIS local (~400k sequências) | benchmarks/tier_bench.py |
Formal (verify_formal) | 7/7 veredictos | — | verificação de tipo do kernel real Lean 4.31.0 | benchmarks/tier_bench.py |
Ramanujan (conjecture_relation) | 6/6 | 0/2 | PSLQ + CF, cada acerto re-verificado ≥25 dígitos | benchmarks/tier_bench.py |
| Moat de aplicabilidade | 15/15 decomp + 6/6 captura | — | pré-condições atômicas, armadilhas de uso incorreto | benchmarks/moat_bench.py |
| FunSearch + web-aug | 14/14 | — | contenção de sandbox (rede / timeout / memória) | benchmarks/tools_bench.py |
A tabela acima, de relance — 0 falsos positivos em todos os níveis (0/8 entradas sem estrutura produziram um falso acerto), 100% de recuperação em conhecidos. Números: RESULTS.md §1–2b.
Agente no ciclo, relatado honestamente (2026-06-10, Claude Fable 5): o mesmo agente sem cabeça recebendo 18 tarefas de matemática COM o servidor MCP da mathlas ao vivo como sua única ferramenta vs SEM quaisquer ferramentas obtém 18/18 vs 15/18. O conjunto original de 10 tarefas está saturado (10/10 em ambos os casos: um modelo de fronteira o passa apenas com conhecimento paramétrico, e dizemos isso claramente), então foi adicionado um conjunto difícil de 8 tarefas onde a verificação, não a recordação, é o gargalo: esse conjunto vai 8/8 COM vs 5/8 SEM. O modelo puro expira na detecção de relação de inteiros de 50 dígitos (PSLQ) e não consegue nomear sequências OEIS obscuras que sombreiam prefixos de Catalan/Fibonacci e só divergem em profundidade. As passagens que o modelo puro obtém são notáveis e nós as relatamos: ele avaliou uma relação constante de 6 termos até 45 dígitos à mão (resíduo 1.475e-27, correto), simulou arredondamento IEEE-754 bit a bit em sua cabeça (com um expoente errado em prosa), e provou uma fórmula tipo Machin exatamente via inteiros gaussianos, tudo em contexto com latência 3-9x maior que uma chamada de ferramenta. Cada verdade fundamental é um cálculo determinístico registrado no bench; tabela completa e proveniência: RESULTS.md §2c. Execução: benchmarks/agent_bench.py.
O índice de 3,68 milhões de documentos. search_existing_math é servido a partir de um índice denso de 3.683.428 documentos (Qwen3-Embedding-8B, 4096-d): o subconjunto 1.34M permissivo CC-BY/CC0 TheoremSearch + 2.34M documentos arXiv-math com slogan incorporado do Dolma, denso + Okapi-BM25 + RRF. Recall honesto de manchete na escala completa de 3,68M: R@1 0.614 / R@10 0.832 consultando pelo corpo bruto de um documento contra sua entrada com slogan — o regime difícil de auto-recall de representação cruzada. (Na construção anterior de 1.635M, o auto-recall mais fácil de mesma representação slogan→slogan era R@1 0.977 / R@10 0.998 em sua divisão retida de 81.833 documentos.)
Corpus aberto no Hugging Face. O lado de texto + metadados desse índice é publicado em kattri15/mathlas-corpus: 3.683.428 documentos em nível de teorema mais a pequena configuração findings, divididos nas configurações theoremsearch, dolma e findings. Inclui slogans, declarações LaTeX, URLs de origem, títulos, rótulos, categorias, contagens de citações quando conhecidas e chaves de proveniência. Não inclui as matrizes de embeddings de 30 GB ou fatias locais de benchmark. Licenças são por configuração: subconjunto TheoremSearch CC BY-SA 4.0, declarações Dolma ODC-BY 1.0 com nossos slogans CC BY 4.0, e descobertas CC BY 4.0. Auditoria 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")
Nível laptop quantizado (opt-in). A matriz fp16 tem 30 GB em disco (~60 GB fp32 residente) — ok na caixa de build, não em um laptop. MATHLAS_QUANTIZED=binary (ou quantized="binary" em HybridRetriever.from_index) serve o MESMO índice a partir de sidecars quantizados com memmap: Hamming de bit de sinal sobre 1,9 GB lista 1000 candidatos, reescore exato escolhe o top-k — medido no índice completo de 3,68M com o mesmo protocolo n=3000 da manchete, é sem perda de recall (R@1 0.6143 vs 0.6140 fp16, R@10 igual em 0.8323; modo int8: R@1 0.6147, 15 GB) a 2,4 s/consulta em 4 threads de CPU. Ressalva honesta: isso encolhe apenas o lado do documento — as consultas ainda precisam ser embedadas pelo mesmo Qwen3-Embedding-8B (um pequeno encoder de 0.6B vive em um espaço vetorial diferente). O nível verdadeiro de pequeno encoder de ponta a ponta é o nível 0.6B abaixo. Números, comando de build e a ressalva completa: docs/QUANTIZED_TIER.md.
Nível laptop 0.6B de ponta a ponta (opt-in). O MESMO corpus de 3.683.428 documentos re-embutido uma vez com Qwen3-Embedding-0.6B (1024-d, alinhado por linha com a meta servida), para que o encoder de consulta em si execute em uma CPU de laptop: MATHLAS_ENCODER=0.6b (compõe com MATHLAS_QUANTIZED=binary). Medido com o protocolo idêntico de representação cruzada n=3000, consultas re-codificadas pelo modelo 0.6B: R@1 0.545 / R@10 0.745 (rescore binário + int8; o scan exato fp16 0.6B é 0.544 / 0.745, então a quantização é novamente sem perdas dentro do nível). O preço honesto vs o nível 8B (0.614 / 0.832) é cerca de 7-9pp de recall; a configuração dual-channel 8B (0.965 / 0.999) permanece o teto de qualidade da caixa grande. A manchete do laptop: pont a ponta 0,67 s/consulta em 4 threads de CPU (0,88 s em 2), codificação de consulta incluída, sobre todos os 3,68M de documentos. Pegada do canal denso: sidecar binário 0,47 GB + encoder 0.6B ~1,2 GB (~1,7 GB; fonte de rescore int8 recomendada 3,77 GB; índice irmão fp16 completo 7,54 GB). No probe só de corpus TheoremSearch-110, o nível pontua Hit@20 8,2% / 10,0% teorema/artigo vs o nível 8B de 10,0% / 11,8% (ambos pisos limitados por licença). Tabelas completas, pegadas e ressalvas: docs/QUANTIZED_TIER.md; build: scripts/build_06b_index.py; eval: scripts/eval_06b_tier.py.
Recuperação dual-channel (opt-in). A manchete 0.614 é uma lacuna de representação cruzada: consultas em forma de declaração LaTeX pesquisadas contra documentos com slogan embutido. Um segundo canal denso embute os mesmos 3.683.428 documentos pela sua declaração LaTeX limpa (Qwen3-Embedding-8B, alinhado por linha, construído por scripts/build_statement_channel.py) e se dobra no ranking denso por max-sim por documento. Medido na mesma amostra n=3000 na escala completa do corpus: R@1 0.614 a 0.965, R@10 0.832 a 0.999. Ressalvas honestas: esse eval é um proxy de auto-recuperação no qual o canal de declaração indexa o próprio texto do qual as consultas são extraídas (uma vantagem de texto exato, como a do BM25); no benchmark de 110 consultas humanas sem vazamento, o aumento é real mas parcial (paper Hit@20 11,8% a 12,7%). E a segunda matriz aproximadamente dobra a RAM de serviço (medida em escala completa: pico de processo de 150 GB para o servidor dual vs ~95 GB canal único; ~2,75 s/consulta de varredura densa dual em 2 threads de CPU), então ela é estritamente opt-in (MATHLAS_STATEMENT_INDEX=/path/index_full_statement.npz, nunca auto-detectada) e não é combinável com o nível quantizado. Números completos e a tabela de nível de serviço: docs/RETRIEVAL_UPGRADE_NOTES.md. O padrão híbrido de produção rrf_k é 10 (medido melhor em cada k testado), mais um blend de rerank cross-encoder opt-in (MATHLAS_RERANK=1, Qwen3-Reranker-0.6B, +1,7pp R@1 de aumento honesto). O backend de rerank é selecionável com MATHLAS_RERANK_MODEL: qwen3 (padrão, Qwen3-Reranker-0.6B, inalterado) ou jina-v3 (jinaai/jina-reranker-v3, arXiv:2509.25085 — um reranker 0.6B "último mas não atrasado" que lidera BEIR na escala 0.6B). Ambos carregam seus pesos preguiçosamente no primeiro uso e recaem na fusão sem rerank (nota honesta em stderr) se torch/transformers ou os pesos estiverem ausentes; um nome de modelo com erro de digitação gera erro em vez de servir silenciosamente o reranker errado. Entregamos a fiação, não um número de benchmark jina — traga seus próprios pesos.
O loop auto-aumentado — vencendo o TheoremSearch
Nas próprias 110 consultas escritas por humanos do TheoremSearch, a mathlas de base atinge um piso de cobertura — o TheoremSearch reteve 85% de seu corpus privado de 9,2M, então 95 artigos-alvo são inalcançáveis para qualquer sistema aberto. A IA então executa o loop: para cada teorema ausente, ela encontra a declaração real na web, a embute com o mesmo Qwen3-Embedding-8B, e add_finding(dense_vec=…) a funde através do canal denso em tempo de execução (re-medido 2026-06-10 no índice servido de 3,68M — a manchete pós-loop reproduz exatamente; a linha de base só do corpus caiu 13,6% → 11,8% no nível de artigo devido aos distratores Dolma adicionados, relatado como está):
| Método | Teorema Hit@20 | Artigo Hit@20 |
|---|---|---|
Google (site:arxiv.org) | — | 37,8% |
| ChatGPT 5.2 com Busca | 19,8% | — |
| Gemini 3 Pro | 27,0% | — |
| TheoremSearch (Qwen3-8B, corpus privado completo de 9,2M) | 45,0% | 56,8% |
| mathlas — linha de base (somente corpus) | 10,0% | 11,8% |
| mathlas — após loop web de auto-aumento | 59,1% (65/110) | 70,0% (77/110) |
Este é o valor do loop, não uma afirmação do corpus nativo. A linha de base de 10,0% é limitada por licenciamento — o TheoremSearch reteve ~85% do seu corpus de 9,2M, então 95/110 artigos-alvo são inalcançáveis para qualquer sistema aberto; o loop web de auto-aumento corrige essa lacuna de cobertura em tempo de execução da IA. A referência do Google é Hit@20 em nível de artigo (nenhum número de teorema relatado); todas as outras referências são Hit@20 em nível de teorema.
Reproduza com benchmarks/webaug_110_bench.py (use a lista de trabalho completa de 82 descobertas _findings_worklist_full.json).
Recuperação ciente da fonte (opt-in). Aumentar o índice de 1,34M → 3,68M teve um custo medido: os 2,34M de documentos Dolma minerados da web empurram artigos canônicos para fora do top-20 (nível de artigo somente corpus 13,6% → 11,8% nessas mesmas 110 consultas). search_existing_math agora aceita source_filter / source_weights opcionais — por exemplo, source_filter={"exclude": ["dolma"]} quando você quer apenas declarações de teoremas canônicos — e excluir dolma recupera totalmente os 13,6% pré-crescimento em nível de artigo (15/110; artigo alcançável-15 15/15 = 100%) com nível de teorema acima do índice antigo (11,8% vs 10,9%). A classificação padrão permanece byte-idêntica (fixada por testes). É um ajuste por intenção de consulta, não uma vitória gratuita: na auto-recuperação n=3000, cujos 65% dos alvos SÃO documentos Dolma, reduzir o peso de dolma é catastrófico para essas consultas (R@10 de alvo-dolma 0,999 → 0,884 no peso 0,5, → 0 quando excluído) — exatamente por isso é enviado como opt-in, desligado por padrão. Também testamos se o canal duplo corrige essa regressão estruturalmente, sem o ajuste: ele recupera parte dela (artigo 11,8% para 12,7%, teorema 10,0% para 10,9% nas configurações padrão), mas não os 13,6% completos, então o ajuste permanece a mitigação documentada neste benchmark. Matriz completa: docs/02_eval_vs_theoremsearch.md.
As 12 ferramentas
search_existing_math ─▶ mapping_scaffold + applicability_checklist ─▶ (AI judges) ─▶ verify_numeric / verify_formal
(own index) (needs↔guarantees, no LLM) (airtight)
Quatro principais — o que a maioria dos agentes usa:
| Ferramenta | O que faz |
|---|---|
search_existing_math(query, k) | consulta → resultados classificados do índice denso + BM25 + RRF de 3,68M de documentos |
identify_constant(value) | um valor real → forma fechada conhecida + proveniência (reavaliação de 50 dígitos) |
verify_numeric(value, closed_form) | veredito de concordância de dígitos — motor diferente, maior precisão |
verify_formal(statement, lean?, proof?) | executa o kernel Lean real — verifica tipos de um trecho, ou passe proof para verificar pelo kernel uma prova Lean 4 completa: VERIFIED_PROOF / REFUTED (o erro exato do kernel, para o loop de reparo) / UNDETERMINED honesto |
Kit de ferramentas completo:
| Ferramenta | O que faz |
|---|---|
search_formal_math(query, backend) | nomes de declarações mathlib + tipos via serviços públicos Loogle (padrão/tipo) + LeanSearch (linguagem natural), com rótulo de proveniência; "serviço indisponível" honesto — com um cache em disco de 7 dias que serve a última resposta boa quando um serviço está fora, claramente rotulado (cached, <age> old) |
identify_sequence(terms) | sequência de inteiros → entradas OEIS correspondentes (correspondência exata de termos) |
applicability_checklist(statement) | hipóteses do resultado como uma lista de verificação atômica para a IA marcar |
mapping_scaffold(problem, statement) | perguntas de necessidades↔garantias + modelo de preenchimento |
conjecture_relation(value) | Ramanujan Machine: PSLQ sobre base rica + conjecturas de CF/recorrência |
funsearch(action, problem_id, …) | harness FunSearch em uma ferramenta — action=evaluate (pontuar em sandbox um programa escrito por IA), register (banco de dados MAP-Elites), status (melhor + few-shot) |
search_directive(problem) | plano de busca na web: consultas arXiv + subcampos + quais ferramentas executar |
add_finding(statement, slogan, source) | ingerir um resultado encontrado na web no corpus ativo |
Todas as ferramentas retornam dados. Nenhuma ferramenta chama um LLM. search_formal_math é a única ferramenta que faz uma chamada web (aos serviços públicos Loogle/LeanSearch); todo o resto é totalmente local.
Verificação de provas — o loop de reparo
verify_formal não apenas verifica tipos de declarações: dê a ele uma proposição e sua prova Lean 4, e o kernel real verifica a declaração completa. mathlas nunca escreve uma prova (a divisão gerador/verificador é absoluta) — mas quando sua prova está errada, o kernel diz exatamente por quê, verbatim, em kernel_error. Isso transforma a escrita de provas em um loop apertado: o agente escreve uma prova → o kernel do mathlas diz exatamente o que está errado → o agente repara e re-chama.
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 ...", ...}
Sem passes falsos, por construção: buracos sorry/admit são REJEITADOS (o próprio Lean sai com 0 em uma prova sorried — mathlas escaneia a fonte e os diagnósticos sorryAx do kernel); um toolchain ausente, um timeout (limite de 60 s), ou um import que este toolchain básico não pode resolver retornam um UNDETERMINED honesto, nunca um veredito. Todo o contrato é fixado por tests/test_proof_check.py (20 testes contra o kernel real Lean 4.31.0: provas corretas de termo e bloco de táticas verificadas, provas erradas refutadas com a mensagem do kernel, provas sorried rejeitadas, 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'
Documentação
RESULTS.md— validação de cada ferramenta, reproduzida, com comandos.docs/methods.md— arquitetura, decisões de design, citações.docs/05_open_dataset.md— o conjunto de dados aberto e o índice.docs/QUANTIZED_TIER.md— o nível de laptop quantizado: recall/pegada/latência medidos.docs/02_eval_vs_theoremsearch.md— o confronto direto de recuperação.docs/REGISTRY_PUBLISH.md— publicação no registro oficial MCP.
Posicionamento — recuperação é o básico; verificação é o fosso
Crédito onde é devido: o sistema mais próximo, TheoremSearch (UW Math AI Lab), agora envia uma API REST de produção e seu próprio endpoint MCP (api.theoremsearch.com/mcp) sobre um corpus de 9,2M de documentos — em recall bruto sobre literatura matemática, é o sistema a ser batido, e "somos nativos MCP, eles são uma ferramenta de laboratório" não é mais um diferencial. Reutilizamos apenas seu subconjunto de dados abertamente licenciado (CC-BY/CC0) como dados brutos para nosso próprio índice — não sua API, MCP, índice ou código.
O sinal da DeepMind, e por que um verificador aberto ainda importa. O AlphaProof Nexus da DeepMind (arXiv:2605.22763) valida precisamente a arquitetura do mathlas — um agente LLM orquestrando um kernel Lean e recursos matemáticos estruturados como OEIS como oráculo de verdade fundamental — mas é somente interno: o artefato público é um despejo de resultados (google-deepmind/alphaproof-nexus-results), não um sistema executável, sem API e sem superfície MCP. Gemini Deep Think e seus pares apenas aguçam a necessidade: conforme os agentes raciocinam mais, um verificador local e determinístico do lado do agente que ele possa chamar de forma barata e offline se torna o gargalo, não o modelo. mathlas permanece a única camada de verificação aberta, sem chave de API, componível via MCP que qualquer agente pode integrar hoje — e agora também ingere o corpus Lean formal-conjectures abertamente licenciado da própria DeepMind (arXiv:2605.13171) como fonte de índice (scripts/fetch_formal_conjectures.py, 3.941 declarações de conjectura Lean, tag de fonte formal_conjectures, incluindo os subconjuntos de avaliação congelados FC100SolvedSet1/FC100OpenSet1).
Nota de nomenclatura: mathlas não está relacionado ao Matlas (matlas.ai, busca de teoremas da Universidade de Pequim, arXiv:2604.17484) — projeto diferente, autores diferentes; a quase-homofonia é coincidência.
O que nenhum concorrente tem é tudo o que acontece após a recuperação:
- Camadas de verificação —
verify_numeric(reavaliação independente de 50 dígitos) everify_formal(uma verificação de tipos real do kernel Lean — incluindo verificação completa de provas com o erro do kernel retornado verbatim para loops de reparo de agentes — ou um UNDETERMINED honesto). A recuperação entrega um candidato; mathlas também pode verificar a afirmação e verificar sua prova dela. applicability_checklist— decompõe um teorema candidato em pré-condições atômicas que a IA verifica uma a uma, capturando aplicações incorretas (intervalo aberto vs fechado, grupo infinito vs finito). Nenhum concorrente tem um.- O loop
add_findingde auto-aumento — a IA encontra na web uma declaração ausente, a incorpora e a funde no índice ativo em tempo de execução: 59,1% vs 45,0% do TheoremSearch em Hit@20 de teorema em seu próprio benchmark de 110 consultas (veja acima). Isso é, até onde sabemos, a primeira instanciação no domínio matemático de um loop RAG com writeback validado — a família de sistemas de recuperação bidirecional que escrevem inferência verificada de volta no armazenamento recuperável (Bidirectional RAG, arXiv:2512.22199), em vez de tratar a recuperação como somente leitura (Self-RAG, arXiv:2310.11511; CRAG, arXiv:2401.15884). O que torna o domínio matemático o lugar certo para isso: o candidato de writeback pode ser verificado deterministicamente (verify_numeric/verify_formal) antes de ser confiável, então o loop cresce o corpus sem o risco de amplificação de alucinação que um loop de writeback genérico carrega. - Disciplina de zero falso-positivo — cada camada retorna um fato verificável independentemente ou um "nada" honesto; a taxa de falso-positivo medida é 0 em todas as camadas (
RESULTS.md). - Grátis, sem chave de API, com rótulo de proveniência — cada resultado carrega de onde veio (
known_constant,conjectured_relation,web_added,external:loogle, …), e o índice é construído 100% a partir de dados abertamente licenciados.
| mathlas | TheoremSearch | LeanSearch / Loogle | Wolfram MCP | sympy-mcp | |
|---|---|---|---|---|---|
| Recuperação matemática informal | ✅ 3,68M docs, aberto | ✅ 9,2M docs (~85% privado) | ❌ (somente declarações mathlib) | ❌ | ❌ |
| Busca formal (mathlib) | ✅ proxy de ambos → uma ferramenta MCP | ❌ | ✅ (é exatamente isso) | ❌ | ❌ |
| Verificação numérica | ✅ reavaliação hermética de 50 dígitos | ❌ | ❌ | ⚠️ avaliação CAS | ⚠️ CAS (sem enquadramento de verificação de afirmação) |
| Verificação formal | ✅ kernel Lean real (declarações e provas completas, erros de loop de reparo) | ❌ | ❌ (busca, não verificação) | ❌ | ❌ |
| Lista de verificação de aplicabilidade | ✅ único | ❌ | ❌ | ❌ | ❌ |
| Corpus de auto-aumento | ✅ add_finding (59,1 vs 45,0 Hit@20) | ❌ | ❌ | ❌ | ❌ |
| Identificação de constante/sequência | ✅ PSLQ + OEIS + Ramanujan-Machine | ❌ | ❌ | ⚠️ alguns | ❌ |
| Rótulos de proveniência | ✅ cada resultado | ❌ | n/a | ❌ | n/a |
| Custo / chave | grátis, sem chave | endpoint gratuito | grátis | chave de API Wolfram paga | grátis |
| MCP | ✅ stdio, one-liner uvx | ✅ endpoint remoto | ❌ (mathlas faz proxy deles) | ✅ | ✅ |
(sympy-mcp é um servidor de manipulação CAS fino — seu escopo mal se sobrepõe: ele reescreve expressões que você dá; mathlas encontra, escopa e verifica matemática existente.)
Registro oficial MCP
mathlas é publicado como io.github.Archerkattri/mathlas (veja docs/REGISTRY_PUBLISH.md e server.json).
mcp-name: io.github.Archerkattri/mathlas