Uma prova matemática pode ocupar dezenas de páginas, depender de resultados construídos ao longo de séculos e exigir que especialistas confiram cuidadosamente cada etapa. O Lean acrescenta uma possibilidade diferente: transformar definições, teoremas e demonstrações em uma linguagem formal que um computador consegue verificar passo a passo.
Lean é uma linguagem de programação de código aberto e, ao mesmo tempo, um assistente de provas, ou proof assistant. O projeto foi iniciado por Leonardo de Moura em 2013, quando ele trabalhava na Microsoft Research, e a primeira versão oficial apareceu em 2014. O Lean 4 foi oficialmente lançado em setembro de 2023.
Essa tecnologia ganhou ainda mais atenção com o avanço da inteligência artificial na matemática. Em 2026, por exemplo, uma versão experimental do Claude, da Anthropic, encontrou um novo resultado relacionado aos zeros da função zeta de Riemann. O TecMaker já explicou como a IA da Anthropic avançou na Hipótese de Riemann sem resolver o problema.
Mas há uma diferença importante entre uma IA propor uma demonstração e um sistema formal verificar se aquela demonstração realmente obedece às regras matemáticas.
É justamente aí que entra o Lean.
Resposta rápida: o que é Lean?
Lean é um assistente de provas e uma linguagem de programação que permite escrever afirmações matemáticas de maneira formal para que um computador possa verificar se uma demonstração é logicamente válida dentro das regras utilizadas pelo sistema.
O site oficial do Lean o descreve como uma linguagem de programação e um assistente de provas voltado à produção de código e demonstrações formalmente verificadas.
Em vez de simplesmente analisar um texto e concluir que ele “parece correto”, Lean transforma a demonstração em uma estrutura formal.
No final do processo, um componente chamado kernel verifica a prova.
Isso faz uma grande diferença.
Uma inteligência artificial pode gerar uma resposta convincente e ainda cometer um erro lógico. No Lean, a construção final precisa obedecer às regras formais reconhecidas pelo sistema.
Quem criou o Lean?
O Lean foi iniciado pelo cientista da computação Leonardo de Moura.
Segundo a documentação oficial, de Moura lançou o projeto em 2013 durante seu período na Microsoft Research. A versão Lean 0.1 foi oficialmente disponibilizada em 16 de junho de 2014.
O próprio Leonardo de Moura informa em sua página profissional que trabalhou durante 17 anos na Microsoft Research antes de ingressar na AWS, em 2023, e que atualmente também atua como arquiteto-chefe e cofundador da Lean Focused Research Organization.
A Lean FRO foi fundada em 2023 por Leonardo de Moura e Sebastian Ullrich para ampliar o desenvolvimento e a aplicação do Lean.
O interessante é que Lean não nasceu especificamente para inteligência artificial.
A aproximação entre assistentes de prova e modelos de IA veio depois e está criando uma nova maneira de pensar sobre descoberta, formalização e verificação matemática.
O que significa um computador verificar uma prova matemática?
Para entender Lean, primeiro precisamos entender uma diferença simples.
Imagine esta afirmação:
Se A é verdadeiro e A implica B, então B é verdadeiro.
Para alguém familiarizado com lógica, essa passagem pode parecer óbvia.
Para um computador, “óbvio” não é uma categoria aceitável.
É preciso definir formalmente:
- quais objetos existem;
- quais hipóteses estão disponíveis;
- quais regras podem ser aplicadas;
- qual resultado deve ser obtido.
Uma demonstração formal deixa essas relações explícitas.
O livro oficial Theorem Proving in Lean 4 apresenta exatamente essa estrutura, passando por proposições, provas, igualdade, quantificadores, indução e táticas.
O computador, então, não precisa “acreditar” no argumento.
Ele verifica se a construção apresentada é válida dentro do sistema lógico utilizado.
Uma analogia: Lean funciona como um fiscal extremamente rigoroso
Imagine a construção de uma ponte.
Um engenheiro pode olhar os cálculos e perceber rapidamente que determinadas etapas estão corretas.
Outro especialista pode aceitar alguns resultados porque eles já são conhecidos na área.
Um sistema formal funciona de maneira diferente.
Ele exige que as peças necessárias estejam definidas de forma suficientemente precisa para que a estrutura possa ser conferida.
Nesse sentido, Lean se parece com um fiscal que não aceita frases como:
“essa parte é evidente”.
É preciso justificar o que está sendo usado.
Isso não significa que o usuário tenha de provar toda a matemática desde o zero. Como veremos adiante, existem bibliotecas enormes contendo resultados já formalizados.
O que é uma prova formal?
Uma prova formal é uma demonstração escrita em uma linguagem suficientemente precisa para ser processada e verificada mecanicamente.
Considere uma afirmação extremamente simples:
2 + 3 = 5
Em Lean, podemos representar um exemplo assim:
example : 2 + 3 = 5 := by decide
O objetivo aqui não é aprender a programar em Lean.
O que importa é perceber que a sentença matemática foi transformada em algo que o sistema consegue interpretar.
A tática decide pode resolver proposições para as quais Lean consegue obter um procedimento de decisão apropriado. A própria documentação explica esse mecanismo.
Em problemas matemáticos avançados, obviamente, a situação pode ser muito mais complexa.
Uma prova pode depender de:
- definições;
- lemas;
- teoremas anteriores;
- estruturas algébricas;
- propriedades analíticas;
- induções;
- cálculos intermediários.
Mas o princípio permanece: cada peça precisa se encaixar formalmente.
O Lean consegue ler uma prova escrita em linguagem comum?
Não da mesma forma que uma pessoa ou um modelo de linguagem lê.
Artigos matemáticos são escritos para matemáticos.
É comum encontrar frases como:
“Do lema anterior, o resultado segue imediatamente.”
Um especialista consegue preencher mentalmente determinadas lacunas.
Lean exige uma representação muito mais explícita.
A transformação de matemática convencional para essa linguagem recebe o nome de formalização.
O que significa formalizar matemática?
Formalizar significa representar uma afirmação e sua demonstração dentro de um sistema lógico preciso.
Pense nesta frase:
“Todo número par pode ser escrito como duas vezes um inteiro.”
Para uma pessoa, o significado parece evidente.
Para formalizá-la, porém, precisamos especificar de forma rigorosa:
- o que é um número inteiro;
- o que significa ser par;
- o significado de “existe”;
- qual operação de multiplicação estamos utilizando.
Esse processo é uma das razões pelas quais formalizar matemática avançada pode exigir bastante trabalho, mesmo quando uma prova informal já é conhecida.
Como o Lean transforma proposições em provas verificáveis?
Lean utiliza uma base chamada teoria de tipos dependentes.
A documentação oficial explica que essa teoria permite representar tanto afirmações matemáticas complexas quanto especificações de hardware e software.
Uma das ideias fundamentais é conhecida como correspondência entre proposições e tipos.
De forma simplificada:
- uma proposição pode ser tratada como um tipo;
- uma prova dessa proposição corresponde a um termo daquele tipo.
Isso cria uma ponte entre programação e lógica.
É uma das razões pelas quais Lean consegue funcionar simultaneamente como linguagem de programação e assistente de provas.
O que é o kernel do Lean?
O kernel é uma das partes mais importantes do sistema.
Lean possui diversas ferramentas sofisticadas capazes de ajudar na construção de uma demonstração.
Mas a confiança final não depende simplesmente dessas ferramentas.
Segundo a documentação oficial, cada tática produz um termo de prova na teoria central do Lean, e esse termo é posteriormente conferido pelo kernel. Isso significa que até um erro em uma tática não deveria transformar automaticamente uma prova inválida em uma prova aceita pelo sistema.
A página oficial sobre validação de provas explica que a aceitação pelo kernel indica que o teorema foi demonstrado a partir das definições, teoremas e axiomas presentes no arquivo e em suas dependências.
Podemos pensar no processo assim:
Afirmação matemática
↓
construção da prova
↓
táticas e ferramentas auxiliam
↓
é produzido um termo formal
↓
o kernel verifica esse termo
É o kernel que funciona como a última barreira formal.
O que são táticas no Lean?
As táticas são ferramentas utilizadas para construir provas.
A referência oficial define uma tática como um programa que modifica o estado atual de uma prova. Ela pode resolver determinado objetivo, gerar novos subproblemas ou falhar se não conseguir avançar.
Uma tática pode, por exemplo:
- simplificar uma expressão;
- aplicar um teorema existente;
- utilizar uma hipótese;
- dividir uma demonstração em casos;
- resolver determinadas equações;
- automatizar operações repetitivas.
Isso torna o processo muito mais prático.
Sem automação, uma pessoa precisaria construir manualmente quantidades enormes de detalhes formais.
Ainda assim, existe uma regra essencial:
a tática não tem autoridade para simplesmente declarar que a prova está correta.
O resultado precisa passar pelo kernel.
Então Lean garante que uma afirmação matemática é verdadeira?
A resposta precisa ser um pouco mais cuidadosa.
Lean consegue verificar que uma determinada afirmação formal possui uma prova válida dentro das regras, definições e axiomas utilizados.
Isso é extremamente forte.
Mas existe uma questão anterior:
A afirmação formalizada representa corretamente aquilo que o pesquisador pretendia provar?
Imagine que alguém queria provar:
Todos os objetos do tipo A possuem determinada propriedade.
Mas, durante a formalização, escreveu uma definição que representa apenas parte desses objetos.
O Lean pode verificar perfeitamente a prova da afirmação formalizada.
Ele não tem como adivinhar que a intenção humana era outra.
Portanto:
verificação formal não elimina especificação, interpretação e revisão científica.
Ela acrescenta uma camada de rigor.
Lean não precisa reconstruir toda a matemática: conheça a Mathlib
Imagine ter que definir novamente números reais, matrizes, limites, grupos, probabilidade e milhares de teoremas toda vez que alguém quisesse formalizar uma nova demonstração.
Seria impraticável.
Por isso existe a Mathlib.
A Mathlib é uma biblioteca comunitária de matemática formalizada para Lean. O próprio projeto a descreve como uma iniciativa para construir uma biblioteca unificada de matemática no assistente de provas.
O panorama oficial da Mathlib mostra a variedade de campos cobertos pela biblioteca.
Podemos pensar nela como uma grande biblioteca científica.
Em vez de demonstrar novamente cada resultado necessário, o pesquisador pode reutilizar definições e teoremas que já foram formalizados.
Assim, novos projetos podem se apoiar em trabalhos anteriores.
Uma prova tradicional e uma prova formal são iguais?
Não exatamente.
A ideia matemática pode ser a mesma, mas a maneira de expressá-la muda bastante.
| Prova matemática convencional | Formalização em Lean |
|---|---|
| Escrita para especialistas humanos | Escrita para interpretação precisa pelo sistema |
| Pode omitir etapas consideradas óbvias | Dependências precisam estar formalmente disponíveis |
| Usa linguagem natural e símbolos | Usa uma linguagem formal |
| Revisada por matemáticos | Verificada pelo kernel e também revisada por humanos |
| Pode depender de intuição contextual | Exige especificações precisas |
Isso não significa que um formato seja simplesmente “melhor” que o outro.
Eles cumprem funções diferentes.
A matemática convencional continua sendo fundamental para comunicação, criatividade e interpretação.
A formalização acrescenta uma camada de verificação mecânica.
O que é sorry em uma prova Lean?
Quem começa a explorar códigos em Lean rapidamente encontra uma palavra curiosa:
sorry
Ela funciona como um marcador temporário.
Durante a construção de uma prova, o desenvolvedor pode utilizar sorry para indicar:
“a demonstração desta parte ainda será preenchida depois.”
O material oficial do Lean explica que sorry pode produzir provisoriamente uma prova, mas gera avisos justamente porque não é uma demonstração válida daquele trecho.
Isso é muito útil durante o desenvolvimento.
Imagine uma prova enorme dividida em dez partes.
Você pode trabalhar primeiro na estrutura geral e depois retornar para preencher os trechos pendentes.
O que significa uma prova “sorry-free”?
Significa que a formalização final não depende desses marcadores provisórios.
Todas as etapas necessárias foram realmente preenchidas com construções verificáveis.
Essa expressão ficou particularmente interessante no caso recente envolvendo a Anthropic e a função zeta de Riemann.
Onde a inteligência artificial entra no Lean?
Lean não é uma inteligência artificial.
Essa distinção precisa ficar muito clara.
O TecMaker possui um guia específico explicando o que são modelos de inteligência artificial e como eles funcionam.
Um modelo de IA pode:
- propor ideias;
- gerar código;
- procurar demonstrações;
- sugerir lemas;
- experimentar caminhos;
- corrigir tentativas.
Lean desempenha outro papel.
Ele fornece uma infraestrutura formal na qual essas construções podem ser verificadas.
Uma maneira simples de guardar essa diferença é:
IA procura. Lean verifica.
Essa combinação é especialmente poderosa.
Imagine uma inteligência artificial produzindo milhares de possíveis etapas de uma demonstração.
Em vez de confiar apenas na linguagem gerada pelo modelo, cada candidato pode ser submetido a um sistema formal.
Se uma construção não obedece às regras, ela é rejeitada.
O caso da Anthropic mostra como essa combinação funciona
Em agosto de 2026, a Anthropic publicou um resultado que tornou essa discussão muito mais concreta.
Uma versão de pesquisa ainda não lançada do Claude tentou trabalhar diretamente na Hipótese de Riemann.
Ela não resolveu a hipótese.
Durante essa tentativa, porém, Claude encontrou uma forma de melhorar um limite conhecido relacionado à proporção de zeros da função zeta localizados sobre a chamada linha crítica. A Anthropic informou uma melhora de 41,6% para aproximadamente 67,2%.
O TecMaker já detalhou como a IA da Anthropic avançou nesse problema sem resolver a Hipótese de Riemann.
E, se você chegou a este artigo sem conhecer o objeto matemático envolvido, vale primeiro entender o que é a função zeta de Riemann e por que ela está ligada aos números primos.
A publicação oficial da Anthropic sobre o experimento informa que Claude também produziu uma prova formalmente verificável de seu resultado.
Essa segunda parte é especialmente importante.
Uma coisa é um modelo de linguagem gerar dezenas de páginas de matemática aparentemente convincentes.
Outra é transformar os resultados em algo que um assistente de provas consiga verificar.
A formalização da Anthropic em Lean 4
A Anthropic também publicou o código da formalização.
O repositório oficial zeta-23-lean descreve uma formalização em Lean 4 e Mathlib, completa e sem sorry, dos teoremas principais apresentados no trabalho.
Isso não significa que Lean tenha “descoberto” a matemática.
Também não significa que a formalização dispense matemáticos.
O exemplo mostra uma divisão de tarefas:
Claude e pesquisadores
exploram e desenvolvem a argumentação.
Formalização em Lean
transforma resultados selecionados em construções formais.
Kernel do Lean
confere se essas construções são aceitas pelas regras do sistema.
Matemáticos
avaliam a interpretação, relevância e relação com o conhecimento existente.
Essa separação é uma das chaves para entender o futuro da inteligência artificial aplicada à matemática.
Lean elimina o risco de erro?
Não completamente.
Mas ele muda bastante o tipo de erro que pode sobreviver à verificação.
Há pelo menos quatro níveis diferentes:
| Pergunta | Principal responsável |
|---|---|
| O problema foi formulado corretamente? | Pesquisadores |
| As hipóteses escolhidas fazem sentido? | Pesquisadores e revisores |
| A demonstração formal segue as regras? | Lean |
| O resultado foi interpretado corretamente? | Comunidade científica |
Lean é extremamente poderoso no terceiro ponto.
Ele não substitui automaticamente os outros três.
Essa distinção é importante para evitar uma manchete perigosa:
“O computador provou, portanto não existe nenhuma possibilidade de erro.”
Ciência é mais complexa do que isso.
O Lean serve apenas para matemática?
Não.
Lean também é uma linguagem de programação e pode ser usado na verificação formal de software.
A teoria de tipos que sustenta o sistema permite representar tanto afirmações matemáticas quanto especificações relacionadas a programas e outros sistemas computacionais.
Isso coloca Lean em uma área de encontro entre:
- matemática;
- lógica;
- ciência da computação;
- engenharia de software;
- inteligência artificial;
- raciocínio automatizado.
É justamente essa interseção que torna a tecnologia tão interessante para o TecMaker.
Lean, Coq e Isabelle são a mesma coisa?
Não.
Lean faz parte de uma família maior de ferramentas conhecidas como assistentes de provas.
Existem outros sistemas importantes utilizados em pesquisa e verificação formal.
Entre eles estão:
- Isabelle;
- Coq, cujo projeto passou também a utilizar o nome Rocq;
- Agda;
- HOL;
- Lean.
Cada um possui suas próprias escolhas de linguagem, fundamentos, bibliotecas e ecossistemas.
O crescimento recente do Lean está muito relacionado à combinação de uma comunidade ativa, à Mathlib, à automação e à aproximação crescente com projetos de inteligência artificial.
Computadores podem descobrir provas matemáticas sozinhos?
Aqui existe uma diferença que merece destaque:
encontrar uma prova e verificar uma prova não são a mesma tarefa.
Lean foi projetado como um ambiente para construir e verificar demonstrações formalmente.
A busca por possíveis provas pode ser realizada por:
- matemáticos;
- programas tradicionais;
- técnicas automatizadas;
- sistemas de inteligência artificial;
- agentes de IA.
Um fluxo moderno pode se parecer com isto:
Problema matemático
↓
humano ou IA explora possíveis soluções
↓
uma demonstração candidata aparece
↓
ela é formalizada
↓
Lean verifica a construção
↓
pesquisadores analisam o significado do resultado
Essa separação também ajuda a entender por que sistemas de agentes de IA são tão interessantes para a ciência.
No TecMaker, já analisamos como agentes de IA estão passando de simples chatbots para sistemas capazes de executar sequências maiores de tarefas.
O que pode mudar na matemática com Lean e inteligência artificial?
A combinação de IA e verificação formal pode mudar principalmente a escala da experimentação.
Um matemático humano não consegue explorar milhares de caminhos simultaneamente durante horas sem interrupção.
Uma infraestrutura de agentes pode.
O problema é que produzir milhares de respostas também significa produzir milhares de possibilidades de erro.
Assistentes de prova introduzem um filtro poderoso.
A IA pode tentar.
Lean pode verificar determinadas construções.
Pesquisadores podem concentrar sua atenção nos resultados que sobrevivem às etapas anteriores.
Isso não elimina a criatividade humana.
Pode mudar onde essa criatividade é empregada.
Em vez de gastar grande parte do tempo conferindo detalhes mecânicos, pesquisadores podem dedicar mais atenção à:
- formulação de novos problemas;
- identificação de padrões;
- escolha de hipóteses;
- interpretação dos resultados;
- criação de novas estratégias;
- conexão entre diferentes áreas da matemática.
Por que formalizar matemática ainda é difícil?
Depois de conhecer Lean, pode surgir uma pergunta natural:
se o computador verifica tudo, por que simplesmente não formalizamos todos os livros de matemática?
Porque traduzir matemática informal para matemática formal é trabalhoso.
Uma página escrita para um especialista pode conter dezenas de conhecimentos implícitos.
O autor não precisa definir cada símbolo novamente.
Não precisa explicar resultados amplamente conhecidos.
Não precisa detalhar cada transformação algébrica.
Lean exige que essas dependências estejam disponíveis de maneira precisa.
A Mathlib reduz enormemente esse trabalho, mas ainda existe uma distância importante entre:
“um matemático entende a demonstração”
e
“a demonstração foi completamente formalizada”.
Inteligência artificial também pode ajudar justamente nessa etapa.
É possível experimentar Lean sem instalar nada?
Sim.
O projeto oferece o Lean Playground, um editor interativo que permite testar Lean diretamente no navegador.
Isso significa que alguém curioso pode experimentar comandos simples sem configurar inicialmente um ambiente completo no computador.
Para quem quiser avançar, a documentação oficial de instalação recomenda o Visual Studio Code com a extensão Lean 4.
Essa possibilidade abre inclusive um caminho interessante para estudantes, professores e pessoas interessadas em lógica e programação.
Lean não precisa ser visto apenas como uma ferramenta de matemáticos profissionais.
Ele também pode ser uma forma diferente de aprender sobre:
- lógica;
- demonstrações;
- programação;
- raciocínio rigoroso.
Lean vai substituir os matemáticos?
Não existe base para afirmar isso.
Lean não escolhe automaticamente quais problemas científicos merecem atenção.
Também não decide sozinho se determinado resultado é profundo, elegante ou útil para outra área.
Uma IA pode auxiliar na exploração.
Um assistente de provas pode auxiliar na verificação.
Mas continuam existindo tarefas essencialmente relacionadas à pesquisa:
- formular boas perguntas;
- reconhecer padrões;
- escolher abstrações;
- avaliar relevância;
- interpretar resultados;
- relacionar uma descoberta com trabalhos anteriores.
O cenário mais interessante, portanto, não é:
computador versus matemático.
É:
matemático + inteligência artificial + verificação formal.
O que isso muda na prática?
Durante muito tempo, os computadores foram associados principalmente a uma capacidade:
calcular muito rápido.
Assistentes de provas ampliam essa visão.
Um computador também pode participar da verificação lógica de argumentos formalizados.
Isso se torna particularmente importante à medida que modelos de IA passam a trabalhar com problemas científicos cada vez mais complexos.
Uma arquitetura possível para o futuro da matemática pode combinar:
Inteligência artificial
para gerar hipóteses e explorar muitas possibilidades.
Lean
para verificar formalmente construções matemáticas.
Mathlib
para fornecer uma base reutilizável de conhecimento já formalizado.
Pesquisadores humanos
para escolher problemas, interpretar resultados e desenvolver novas ideias.
O ganho não vem de uma única tecnologia.
Vem da combinação.
Perguntas frequentes sobre Lean e provas matemáticas
O que é Lean em matemática?
Lean é uma linguagem de programação e um assistente de provas que permite representar definições, teoremas e demonstrações em uma forma que pode ser verificada por computador. O projeto é de código aberto e sua documentação está disponível no site oficial do Lean.
Para que serve o Lean?
Lean pode ser utilizado para formalizar matemática, verificar demonstrações e desenvolver software formalmente verificado. Sua teoria de tipos permite expressar tanto afirmações matemáticas quanto especificações computacionais.
Lean é uma inteligência artificial?
Não. Lean é um assistente de provas e uma linguagem de programação. Uma inteligência artificial pode sugerir ou construir partes de uma demonstração, enquanto Lean pode verificar a estrutura formal produzida.
Como Lean sabe que uma prova está correta?
Lean produz termos formais que são verificados por seu kernel. Cada tática precisa resultar em uma construção aceita pelo núcleo lógico do sistema.
O que é Mathlib?
Mathlib é uma biblioteca comunitária de matemática formalizada para Lean. Ela reúne definições e teoremas reutilizáveis, reduzindo a necessidade de reconstruir a base matemática a cada novo projeto.
O que significa sorry no Lean?
sorry é um marcador provisório usado durante o desenvolvimento quando determinada parte da prova ainda não foi preenchida. Lean permite seu uso, mas gera avisos porque ele não representa uma demonstração completa daquele trecho.
O que significa uma formalização “sorry-free”?
Significa que a prova final não depende desses marcadores provisórios. As etapas necessárias foram substituídas por construções efetivamente verificáveis.
A Anthropic usou Lean na pesquisa sobre a Hipótese de Riemann?
A Anthropic publicou uma formalização em Lean 4 e Mathlib associada ao resultado encontrado durante sua investigação de um problema relacionado à Hipótese de Riemann. O repositório oficial da formalização a descreve como completa e sem sorry nos teoremas formalizados.
Posso testar Lean gratuitamente?
Sim. É possível utilizar o Lean Playground diretamente no navegador.
Conclusão: IA pode procurar, mas alguém ainda precisa verificar
Lean representa uma transformação importante na relação entre matemática e computadores.
Durante décadas, máquinas foram utilizadas principalmente para executar cálculos que seriam lentos ou impraticáveis para uma pessoa.
Assistentes de provas acrescentaram uma nova possibilidade:
verificar argumentos matemáticos formalmente.
sso não transforma o computador em um matemático infalível.
Também não elimina a necessidade de revisão humana.
Mas cria uma camada de rigor especialmente valiosa em uma época em que sistemas de inteligência artificial conseguem gerar enormes quantidades de código, hipóteses e raciocínios matemáticos.
O caso da Anthropic tornou essa combinação particularmente visível.
Primeiro, uma IA explorou centenas de caminhos em um problema relacionado à função zeta.
Depois, parte do resultado pôde ser transformada em matemática formal verificável.
A sequência mostra um possível modelo para a ciência assistida por inteligência artificial:
explorar → formular → formalizar → verificar → interpretar.
E estamos apenas começando a descobrir o que essa combinação pode produzir.
Se você quiser continuar por essa trilha, leia também o que é a função zeta de Riemann e entenda como a IA da Anthropic conseguiu avançar em um problema relacionado à Hipótese de Riemann.
A Equipe TecMaker é o núcleo editorial e de testes do portal, dedicada a trazer análises imparciais, comparativos de produtos e as últimas notícias do universo da tecnologia. Nosso objetivo é decodificar a inovação e ajudar nossos leitores a fazerem as melhores escolhas no mercado digital e de dispositivos emergentes.
