A startup Math Inc., que no Brasil poderia ser chamada de “Matemática S.A.”, está sediada na Califórnia e concentra seus esforços na formalização da matemática. Esse processo envolve a transcrição de definições e teoremas para sistemas de linguagem formal, como o Lean, assunto abordado aqui na semana passada.
A empresa possui uma visão extremamente ousada, sugerindo que estamos testemunhando o início de uma nova era de ouro para a matemática. No entanto, seu objetivo mais concreto é viabilizar a verificação automática da correção dos raciocínios, assegurando que os teoremas sejam comprovados com rigor absoluto. Para isso, a Math Inc. conta com a colaboração de alguns dos maiores especialistas da atualidade, incluindo Maryna Viazovska e Terence Tao, ambos vencedores da medalha Fields.
Em janeiro de 2024, Tao, em parceria com o colega Alex Kontorovich, propôs à comunidade científica que o teorema dos números primos fosse formalizado em Lean. Esse teorema, um dos resultados mais significativos da teoria dos números, foi demonstrado de forma independente em 1896 pelo francês Jacques Hadamard e pelo belga Charles de la Vallée Poussin.
Em termos simplificados, o teorema afirma que a porcentagem de números primos entre 1 e N é inversamente proporcional ao número de dígitos de N. Isso significa que, à medida que N aumenta, os primos se tornam cada vez mais escassos. A demonstração desse teorema envolve conceitos matemáticos extremamente profundos, e desde o início ficou claro que a formalização representaria um desafio altamente complexo. Kontorovich e Tao dedicaram 18 meses ao problema, obtendo avanços parciais ao longo do período.
Em 10 de março passado, a Math Inc. anunciou que concluiu a tarefa utilizando uma nova inteligência artificial chamada Gauss, descrita como “um agente de autoformalização pioneiro, projetado para auxiliar matemáticos na verificação formal de teoremas”. De acordo com a empresa, o agente é capaz de trabalhar de forma autônoma por horas, sem intervenção humana, o que acelera drasticamente o processo.
Em apenas três semanas, Gauss transcreveu a prova para aproximadamente 25 mil linhas de código Lean, incluindo mais de mil definições e teoremas auxiliares. Para efeito de comparação, o maior projeto desse tipo já realizado produziu 500 mil linhas, mas levou mais de uma década para ser concluído. A expectativa é que futuros agentes de formalização se tornem cada vez mais autônomos e rápidos.
Todos esses códigos agora integram a MathLib, o repositório mundial do Lean, que já conta com cerca de 2 milhões de linhas, cobrindo 350 mil teoremas e definições. Esse volume equivale a aproximadamente 50 livros avançados de matemática. Esse material está disponível para ser utilizado na validação de novos teoremas, o que indica que, à medida que o projeto de formalização avança, ele também tende a se acelerar.
A Math Inc. afirma acreditar que isso também tornará viável o treinamento de inteligências artificiais universalistas, capazes de dominar todas as áreas da matemática. Entre os seres humanos, os últimos universalistas foram Henri Poincaré e David Hilbert, há um século.
No entanto, ainda não chegamos lá. Antes disso, será necessário superar inúmeros desafios. Um exemplo natural são os teoremas de empacotamento de esferas nas dimensões 8 e 24, que renderam a medalha Fields a Viazovska. Esse tema fica para o encerramento desta série, na próxima semana.
