Math Inc. (no Brasil seria “Matemática S.A.”) é uma startup baseada na Califórnia dedicada à formalização da matemática, ou seja, à transcrição de definições e teoremas para sistemas formais de linguagem como o Lean, de que falei aqui na semana passada.
A empresa tem uma visão extremamente ambiciosa (“Aqueles que estão prestando atenção podem sentir a alvorada de uma nova era de ouro da matemática”…), mas o objetivo mais concreto é poder verificar, automaticamente, que os raciocínios estão corretos e, portanto, esses teoremas estão realmente provados com rigor total. Para isso, contam entre seus colaboradores com alguns dos melhores especialistas da atualidade, como Maryna Viazovska e Terence Tao, ambos ganhadores da medalha Fields.
Em janeiro de 2024, Tao e seu colega Alex Kontorovich propuseram à comunidade científica formalizar em Lean o teorema dos números primos, um dos mais importantes resultados da teoria dos números, provado em 1896, independentemente, pelo francês Jacques Hadamard e pelo belga Charles de la Vallée Poussin.
Esse teorema afirma, grosseiramente falando, que a porcentagem dos números de 1 a N que são primos é inversamente proporcional ao número de dígitos de N. Em particular, os primos vão ficando cada vez mais raros quando aumentamos N. A demonstração usa ideias matemáticas muito profundas, era claro desde o início que a formalização seria um desafio altamente não trivial. Kontorovich e Tao trabalharam no problema durante 18 meses, com avanços parciais.
Então, em 10 de março passado, a Math Inc. anunciou ter completado a tarefa por meio de uma nova inteligência artificial, Gauss, “um agente de autoformalização pioneiro concebido para auxiliar matemáticos na verificação formal de teoremas”. Segundo a empresa, o agente pode trabalhar durante horas de forma autônoma, sem ajuda de humanos, o que agiliza dramaticamente o trabalho.
Em apenas três semanas, Gauss transcreveu a prova para cerca de 25 mil linhas de código Lean, contendo mais de um milhar de definições e teoremas auxiliares. A título de comparação, o maior projeto desse tipo já realizado gerou 500 mil linhas, mas demorou mais de uma década (!) para ser executado. A expectativa é que futuros agentes de formalização sejam cada vez mais autônomos e rápidos.
Todos esses códigos agora fazem parte da MathLib, o repositório mundial de Lean, que já alcança cerca de 2 milhões de linhas, cobrindo 350 mil teoremas e definições. É o equivalente a uns 50 livros avançados de matemática. E esse material está disponível para ser invocado na validação de novos teoremas, o que significa que à medida que o projeto de formalização avança, ele também deverá se acelerar.
A Math Inc. diz acreditar que isso também tornará viável treinar inteligências artificiais universalistas, dominando todas as áreas da matemática. Entre os humanos, os últimos universalistas foram Henri Poincaré e David Hilbert, um século atrás.
Mas ainda não estamos lá, antes será necessário vencer inúmeros desafios. Um exemplo natural: os teoremas de empacotamento de esferas em dimensões 8 e 24 que valeram a Viazovska a medalha Fields. Fica para o encerramento desta série, na semana que vem.
Fonte ==> Folha SP – TEC
