Um desenvolvedor Mathlib na ISTA: o ‘projeto paralelo’ do estudante de graduação Martin Dvorák
Matemática é um termo abrangente que une diversas disciplinas com diferentes convenções. Além disso, explicar toda a matemática enquanto se prova teoremas é quase impossível, e o processo de revisão por pares é notoriamente lento. Martin Dvorák, estudante de pós-graduação na Grupo Kolmogorov no Instituto de Ciência e Tecnologia da Áustria (ISTA) é desenvolvedor do Mathlib, digitalizando conceitos comprovados em todas as disciplinas matemáticas. Descubra como ele faz isso ‘ao lado’.
Uma Biblioteca de Alexandria do século XXI com matemática digitalizada está sendo construída, um tijolo de cada vez, num esforço coletivo de uma pequena comunidade de matemáticos meticulosos em todo o mundo. Eles são movidos pela visão de, um dia, centralizar todo o conhecimento matemático da humanidade em todas as disciplinas. Mas, além de simplesmente arquivar conceitos matemáticos, este trabalho meticuloso das formigas está ajudando-as a revolucionar a matemática, tornando-a acessível à descoberta impulsionada pela inteligência artificial (IA).
Esta nova Biblioteca de Alexandria de toda a matemática é um software de computador chamado “Mathlib”. Centraliza conceitos matemáticos que são verdadeiros em todas as disciplinas matemáticas, tornando-os uma base de “verdade” para todas as entradas futuras. Nascida de “Lean”, uma linguagem de programação eficiente e organizada para desenvolvimento de software lançada em 2013, Mathlib significa ‘Biblioteca matemática Lean’. “Lean é a linguagem de código da lógica, e Mathlib é a biblioteca construída sobre essa lógica”, diz o estudante Martin Dvorák, hoje o único desenvolvedor de Mathlib no Instituto de Ciência e Tecnologia da Áustria (ISTA). Atualmente é o único contribuidor ativo na Áustria.
“Sou apaixonado por ajudar a digitalizar toda a matemática conhecida pela humanidade para impulsionar o progresso da matemática, e estou fazendo isso como um ‘projeto paralelo’. É claro que isso também me ajuda em minha rotina de provar teoremas como estudante de pós-graduação. Eu provar tudo interativamente no Lean, com a tremenda ajuda do Mathlib. Quanto mais lemas – teoremas intermediários – são incorporados ao Mathlib, menos tenho que provar teoremas do zero.”
Lógica ‘Lean’, do código do software à prova matemática
Quando o Lean foi lançado, os matemáticos reconheceram rapidamente que o seu poder na verificação da validade do código de software era muito semelhante ao da verificação de uma prova matemática. Esta era uma oportunidade que eles não podiam perder. A necessidade deles de uma biblioteca matemática nova, bem planejada e cuidadosamente construída era real demais.
Assistentes de prova computacional não são novos. O primeiro programa desse tipo, “Automat”, foi lançado na década de 1960. Seguiram-se então “Mizar” em 1973 e “” em 1989, dois assistentes de prova que foram amplamente utilizados entre os matemáticos. Mas em vez de procurar centralizar o conhecimento matemático no Coq, os seus utilizadores definiam de forma independente problemas que apenas lhes interessavam, muitas vezes utilizando uma linguagem única. Isso fez com que Coq crescesse como uma cidade não planejada, com muitas bibliotecas menores e independentes fazendo com que a plataforma parecesse confusa. O Lean proporcionou aos matemáticos um novo começo muito necessário, aproveitando os desafios do passado. “O Lean permitiu-nos chegar a um acordo colectivo sobre uma interpretação da matemática escrita por humanos. Com esta ferramenta, podemos desenvolver conceitos que permanecem verdadeiros em todas as circunstâncias e codificá-los inequivocamente num software de computador, acessível a todos”, diz Dvorák. É assim que a ‘comunidade Lean’ de desenvolvedores trabalha na construção do Mathlib, um tijolo de cada vez.
Uma ‘pirâmide de evidências’ à prova de balas
Dvorák e seus colegas desenvolvedores do Mathlib em todo o mundo estão construindo uma base sólida de matemática. Partindo de problemas específicos de um ramo da matemática, procuram as versões mais gerais e amplamente aplicáveis de conceitos matemáticos. Provar teoremas no Lean é um processo interativo entre o desenvolvedor e o computador, explica Dvorák. O desenvolvedor dá cada vez mais dicas sobre como verificar um conceito, e o software o estabelece com base nos elementos já verificados. Os desenvolvedores do Mathlib também extraem padrões de pensamento matemático e os codificam como ‘táticas’ – blocos de construção lógicos – no Lean.
Assim, o Mathlib funciona como uma pirâmide de evidências. Além de tornar o Mathlib logicamente à prova de balas, a biblioteca também é altamente ágil. “Nosso trabalho como desenvolvedores é garantir que a pirâmide tenha bases sólidas, mas flexíveis. Quando você adiciona um novo ‘tijolo’ ao Mathlib, o PC pode recompilar toda a pirâmide durante a noite, desmontando tudo e reconstruindo-a tijolo por tijolo.” diz Dvorák. Isso garante que tudo seja verificado por computador quanto à correção matemática. Assim, quando um usuário – seja humano ou IA, como AlphaProof do Google DeepMind – insere um problema junto com instruções sobre como prová-lo, o Mathlib pode executar rapidamente as verificações necessárias e fornecer uma prova gerada por computador.
Investindo no futuro da matemática
Grandes resultados matemáticos dependem de centenas de artigos matemáticos, mas o erro humano torna impossível garantir que o raciocínio esteja totalmente correto. “Mas se você basear sua prova em lemas do Mathlib, você terá a maior garantia de que tudo o que você usa foi verificado por computador quanto à exatidão absoluta”, diz Dvorák.
Além de tornar as provas matemáticas à prova de balas, o Mathlib também democratiza a matemática. Impulsiona colaborações em larga escala entre matemáticos, superando barreiras importantes de “confiança” científica na área. “O Mathlib pode dizer em cinco segundos se você cometeu um erro flagrante em seu raciocínio. Isso economiza uma quantidade incrível de tempo em comparação com a espera de vários meses por uma revisão humana”, diz Dvorák. Por outro lado, é extremamente satisfatório quando o computador exibe ‘objetivos cumpridos’. Então você sabe que ninguém mais pode refutar o que você fez.”
Dvorák está visivelmente orgulhoso da sua contribuição para este colossal trabalho colaborativo, mas está perfeitamente consciente de que o Mathlib, tal como a matemática, nunca poderá ser “terminado”. “Não sabemos como será a matemática daqui a algumas décadas. Na verdade, nem sabemos a extensão do conhecimento matemático da humanidade neste momento. maneiras que nem podemos imaginar hoje.”
