Uma pequena comunidade de matemáticos está usando um programa de software chamado Lean para construir um novo repositório digital. Eles esperam que represente o futuro de seu campo.
Todos os dias, dezenas de matemáticos com ideias semelhantes se reúnem em um fórum online chamado Zulip para construir o que acreditam ser o futuro de sua área.
Eles são todos devotos de um programa de software chamado Lean. É um “assistente de prova” que, em princípio, pode ajudar os matemáticos a escrever provas. Mas antes que o Lean possa fazer isso, os próprios matemáticos precisam inserir manualmente a matemática no programa, traduzindo milhares de anos de conhecimento acumulado em uma forma que o Lean possa entender.
Para muitas das pessoas envolvidas, as virtudes do esforço são quase evidentes.
“É fundamentalmente óbvio que, quando você digitaliza algo, pode usá-lo de novas maneiras”, disse Kevin Buzzard, do Imperial College London. “Vamos digitalizar a matemática e isso vai torná-la melhor.”
Digitalizar matemática é um sonho antigo. Os benefícios esperados variam do mundano – computadores dando notas aos deveres de casa dos alunos – ao transcendente: usar a inteligência artificial para descobrir novas matemáticas e encontrar novas soluções para velhos problemas. Os matemáticos esperam que os assistentes de prova também possam revisar as submissões de periódicos, encontrando erros que os revisores humanos ocasionalmente deixam passar, e lidar com o trabalho técnico tedioso que é necessário para preencher todos os detalhes de uma prova.
Mas, primeiro, os matemáticos que se reúnem em Zulip devem fornecer a Lean o que equivale a uma biblioteca de conhecimentos matemáticos de graduação, e eles estão apenas na metade do caminho. O Lean não resolverá problemas em aberto tão cedo, mas as pessoas que estão trabalhando nele têm quase certeza de que em alguns anos o programa pelo menos será capaz de entender as questões do exame final do último ano.
E depois disso, quem sabe? Os matemáticos que participam desses esforços não antecipam totalmente para que serve a matemática digital.
“Não sabemos realmente para onde estamos indo”, disse Sébastien Gouëzel, da Universidade de Rennes.
Você planeja, costeletas enxutas
Durante o verão, um grupo de usuários experientes do Lean conduziu um workshop online chamado “Lean para o Matemático Curioso”. Na primeira sessão, Scott Morrison, da University of Sydney, demonstrou como escrever uma prova no programa.
Ele começou digitando a instrução que queria provar na sintaxe que o Lean entende. Em inglês simples, significa “Existem infinitamente muitos números primos.” Existem várias maneiras de provar essa afirmação, mas Morrison queria usar uma ligeira modificação da primeira descoberta, a prova de Euclides de 300 aC, que envolve a multiplicação de todos os primos conhecidos e a adição de 1 para encontrar um novo primo (seja o próprio produto ou um de seus divisores será primo). A escolha de Morrison refletiu algo básico sobre o uso do Lean: o usuário tem que ter a grande ideia da prova por conta própria.
“Você é responsável pela primeira sugestão”, disse Morrison em uma entrevista posterior.
Depois de digitar a declaração e selecionar uma estratégia, Morrison passou alguns minutos delineando a estrutura da prova: ele definiu uma série de etapas intermediárias, cada uma das quais era relativamente simples de provar por conta própria. Embora o Lean não consiga definir a estratégia geral de uma prova, muitas vezes pode ajudar a executar etapas menores e concretas. Ao quebrar a prova em subtarefas gerenciáveis, Morrison era um pouco como um chef instruindo cozinheiros de linha a cortar uma cebola e cozinhar um ensopado. “É neste ponto que você espera que o Lean assuma o controle e comece a ser útil”, disse Morrison.
O Lean executa essas tarefas intermediárias usando processos automatizados chamados “táticas”. Pense neles como algoritmos curtos adaptados para realizar um trabalho muito específico.
Enquanto trabalhava em sua prova, Morrison executou uma tática chamada “busca na biblioteca”. Ele vasculhou o banco de dados de resultados matemáticos de Lean e retornou alguns teoremas que julgou poder preencher os detalhes de uma seção específica da prova. Outras táticas realizam diferentes tarefas matemáticas. Um, chamado “linarito”, pode pegar um conjunto de desigualdades entre, digamos, dois números reais e confirmar para você que uma nova desigualdade envolvendo um terceiro número é verdadeira: Se a é 2 e b é maior que a, então 3a + 4b é maior que 12. Outro faz a maior parte do trabalho de aplicação de regras algébricas básicas, como associatividade.
“Dois anos atrás, você teria que [aplicar a propriedade associativa] no Lean”, disse Amelia Livingston, estudante de matemática no Imperial College London que está aprendendo Lean com Buzzard. “Então [alguém] escreveu uma tática que pode fazer tudo por você. Cada vez que o uso, fico muito feliz. ”
Ao todo, Morrison levou 20 minutos para concluir a prova de Euclides. Em alguns lugares, ele mesmo preencheu os detalhes; em outros, ele usou táticas para fazer isso por ele. Em cada etapa, Lean verificou se seu trabalho era consistente com as regras lógicas subjacentes do programa, que são escritas em uma linguagem formal chamada teoria dos tipos dependentes.
“É como um aplicativo de sudoku. Se você fizer um movimento que não é válido, vai virar buzz “, disse Buzzard. No final, Lean certificou que a prova de Morrison funcionou.
O exercício foi empolgante como sempre é quando a tecnologia intervém para fazer algo que você costumava fazer. Mas a prova de Euclides existe há mais de 2.000 anos. Os tipos de problemas com os quais os matemáticos se preocupam hoje são tão complicados que Lean ainda não consegue entender as perguntas, muito menos apoiar o processo de respondê-las.
“Provavelmente levará décadas até que esta seja uma ferramenta de pesquisa”, disse Heather Macbeth, da Fordham University, uma colega usuária do Lean.
Portanto, antes que os matemáticos possam trabalhar com o Lean nos problemas com os quais realmente se preocupam, eles precisam equipar o programa com mais matemática. Na verdade, essa é uma tarefa relativamente simples.
“Lean ser capaz de entender algo é basicamente uma questão de seres humanos terem [livros de matemática traduzidos] na forma que Lean pode entender”, disse Morrison.
Infelizmente, direto não significa fácil, especialmente considerando que, para muitos matemáticos, os livros didáticos não existem de verdade.
Conhecimento Espalhado
Se você não estudou matemática avançada, o assunto provavelmente parece exato e bem documentado: Álgebra I leva à álgebra II, pré-cálculo leva ao cálculo, e está tudo disposto ali nos livros didáticos, chave de respostas no verso.
Mas a matemática do ensino médio e da faculdade – até mesmo muita matemática da pós-graduação – é uma parte cada vez menor do conhecimento geral. A grande maioria é muito menos organizada.
Existem áreas enormes e importantes da matemática que nunca foram totalmente escritas. Eles estão armazenados nas mentes de um pequeno círculo de pessoas que aprenderam seu subcampo da matemática com pessoas que aprenderam com a pessoa que o inventou – ou seja, existe quase como folclore.
Existem outras áreas onde o material básico foi escrito, mas é tão longo e complicado que ninguém foi capaz de verificar se está totalmente correto. Em vez disso, os matemáticos simplesmente têm fé.
“Contamos com a reputação do autor. Sabemos que ele é um gênio e um cara cuidadoso, então deve estar correto “, disse Patrick Massot, da Universidade Paris-Saclay.
Esta é uma das razões pelas quais os assistentes de prova são tão atraentes. Traduzir a matemática para uma linguagem que um computador pode entender força os matemáticos a finalmente catalogar seu conhecimento e definir objetos com precisão.
Assia Mahboubi, do instituto nacional de pesquisa francês Inria, relembra a primeira vez que percebeu o potencial de uma biblioteca digital tão ordenada: “Foi fascinante para mim que alguém pudesse capturar, em teoria, toda a literatura matemática pela linguagem pura da lógica e armazenamento um corpus de matemática em um computador e verifique-o e navegue usando esses softwares. ”
Lean não é o primeiro programa com esse potencial. O primeiro, chamado Automath, foi lançado na década de 1960, e Coq, um dos assistentes de prova mais usados hoje, foi lançado em 1989. Os usuários do Coq formalizaram muita matemática em sua linguagem, mas esse trabalho foi descentralizado e desorganizado . Os matemáticos trabalharam em projetos que os interessaram e apenas definiram os objetos matemáticos necessários para realizar seus projetos, muitas vezes descrevendo esses objetos de maneiras únicas. Como resultado, as bibliotecas do Coq parecem confusas, como uma cidade não planejada.
“Coq é um homem velho agora e tem muitas cicatrizes”, disse Mahboubi, que trabalhou extensivamente com o programa. “Tem sido mantido de forma colaborativa por muitas pessoas ao longo do tempo e tem defeitos conhecidos devido à sua longa história.”
Em 2013, um pesquisador da Microsoft chamado Leonardo de Moura lançou o Lean. O nome reflete o desejo de Moura de criar um programa com um design eficiente e organizado. Ele pretendia que o programa fosse uma ferramenta para verificar a precisão do código do software, não matemática. Mas verificar a exatidão do software, ao que parece, é muito parecido com verificar uma prova.
“Construímos o Lean porque nos preocupamos com o desenvolvimento de software, e existe uma analogia entre construir matemática e construir software”, disse de Moura.
Quando o Lean foi lançado, havia muitos outros assistentes de prova disponíveis, incluindo Coq, que é o mais semelhante ao Lean – os fundamentos lógicos de ambos os programas são baseados na teoria do tipo dependente. Mas o Lean representou uma chance de começar do zero.
Os matemáticos gravitaram para ele rapidamente. Eles adotaram o programa com tanto entusiasmo que começaram a consumir o tempo de de Moura com suas questões de desenvolvimento específicas de matemática. “Ele ficou um pouco cansado de ter que gerenciar os matemáticos e disse:’ Que tal vocês criarem um repositório separado? ‘”, Disse Morrison.
Matemáticos criaram essa biblioteca em 2017. Eles a chamaram de mathlib e avidamente começaram a preenchê-la com o conhecimento matemático do mundo, tornando-a uma espécie de Biblioteca de Alexandria do século 21. Os matemáticos criaram e carregaram peças de matemática digitalizada, construindo gradualmente um catálogo para o Lean se basear. E como o mathlib era novo, eles podiam aprender com as limitações de sistemas mais antigos, como o Coq, e prestar atenção extra em como organizavam o material.
“Há um verdadeiro esforço para fazer uma biblioteca monolítica de matemática em que todas as peças funcionem com todas as outras”, disse Macbeth.
O Mathlib de Alexandria
A página inicial do mathlib apresenta um painel em tempo real que mostra o progresso do projeto. Ele tem uma tabela de classificação dos principais contribuidores, classificados pelo número de linhas de código que eles criaram. Há também uma contagem contínua da quantidade total de matemática que foi digitalizada: no início de outubro, mathlib continha 18.416 definições e 38.315 teoremas.
Esses são os ingredientes que os matemáticos podem misturar no Lean para fazer matemática. No momento, apesar desses números, é uma despensa limitada. Não contém quase nada de análises complexas ou equações diferenciais – dois elementos básicos de muitos campos da matemática superior – e não sabe o suficiente para sequer declarar qualquer um dos problemas do Prêmio Millennium, a lista do Clay Mathematics Institute dos problemas mais importantes em matemática .
Mas mathlib está lentamente preenchendo. A obra tem ares de construção de celeiro. Em Zulip, os matemáticos identificam as definições que precisam ser criadas, se oferecem para escrevê-las e fornecem rapidamente feedback sobre o trabalho uns dos outros.
“Qualquer pesquisador matemático pode olhar para mathlib e ver 40 coisas que está faltando”, disse Macbeth. “Então você decide preencher um desses buracos. É realmente uma gratificação instantânea. Alguém o lê e comenta em 24 horas. ”
Muitas das adições são pequenas, como Sophie Morel da École Normale Supérieure em Lyon descobriu durante o workshop “Lean for the Curious Mathematician” neste verão. Os organizadores da conferência deram aos participantes afirmações matemáticas relativamente simples para serem comprovadas no Lean como prática. Enquanto trabalhava em um deles, Morel percebeu que sua prova pedia um lema – um tipo de resultado intermediário curto – que mathlib não tinha.
“Era uma coisa muito pequena sobre a álgebra linear que de alguma forma ainda não existia. As pessoas que escrevem mathlib tentam ser minuciosas, mas você nunca consegue pensar em tudo “, disse Morel, que codificou o lema de três linhas sozinha.
Outras contribuições são mais importantes. No último ano, Gouëzel tem trabalhado em uma definição de “variedade suave” para mathlib. Variedades suaves são espaços – como linhas, círculos e a superfície de uma bola – que desempenham um papel fundamental no estudo da geometria e da topologia. Eles também costumam apresentar grandes resultados em áreas como teoria e análise dos números. Você não poderia esperar fazer a maioria das formas de pesquisa matemática sem definir uma.
Mas as variedades suaves vêm em diferentes formas, dependendo do contexto. Eles podem ser dimensionais finitos ou dimensionais infinitos, ter “fronteira” ou não, e ser definidos em uma variedade de sistemas numéricos, como os números reais, complexos ou p-ádicos. Definir uma variedade suave é quase como tentar definir o amor: você o reconhece quando o vê, mas qualquer definição estrita provavelmente excluirá alguns exemplos óbvios do fenômeno.
“Para uma definição básica, você não tem escolha [de como você a define]”, disse Gouëzel. “Mas com objetos mais complicados, existem talvez 10 ou 20 maneiras diferentes de formalizá-los.”
Gouëzel teve que manter um ato de equilíbrio entre especificidade e generalidade. “Minha regra era, eu conheço 15 aplicações de manifolds que eu gostaria de poder declarar”, disse ele. “Mas eu não queria que a definição fosse muito geral, porque então você não pode trabalhar com ela.”
A definição que ele criou preenche 1.600 linhas de código, tornando-a bem longa para uma definição mathlib, mas talvez leve em comparação com as possibilidades matemáticas que ela abre no Lean.
“Agora que temos a linguagem, podemos começar a provar teoremas”, disse ele.
Encontrar a definição certa para um objeto, no nível certo de generalidade, é uma grande preocupação dos matemáticos que constroem a biblioteca matemática. Seus criadores esperam definir objetos de uma forma que seja útil agora, mas flexível o suficiente para acomodar os usos imprevistos que os matemáticos podem ter para esses objetos.
“Há uma ênfase em que tudo seja útil no futuro”, disse Macbeth.
A prática torna perfectoide
Mas o Lean não é apenas útil – ele oferece aos matemáticos a chance de se envolver com seu trabalho de uma nova maneira. Macbeth ainda se lembra da primeira vez que ela tentou um assistente de prova. Era 2019 e o programa era Coq (embora ela use Lean agora). Ela não conseguia parar.
“Em um fim de semana louco, passei 12 horas por dia [nisso]”, disse ela. “Era totalmente viciante.”
Outros matemáticos falam sobre a experiência da mesma maneira. Eles dizem que trabalhar no Lean é como jogar um videogame – completo com a mesma corrida neuroquímica baseada em recompensa que torna difícil desligar o controle. “Você pode fazer 14 horas por dia com ele e não se cansar e se sentir meio alto o dia todo”, disse Livingston. “Você está constantemente recebendo reforço positivo.”
Ainda assim, a comunidade Lean reconhece que, para muitos matemáticos, simplesmente não há níveis suficientes para jogar.
“Se você quantificasse quanto da matemática é formalizado, eu diria que é bem menos que um milésimo de um por cento”, disse Christian Szegedy, um engenheiro do Google que está trabalhando em sistemas de inteligência artificial que ele espera que consigam para ler e formalizar livros de matemática automaticamente.
Mas os matemáticos estão aumentando a porcentagem. Embora hoje mathlib contenha a maior parte do conteúdo da matemática do segundo ano de graduação, os colaboradores esperam adicionar o restante do currículo dentro de alguns anos – um marco significativo.
“Nos 50 anos em que esses sistemas existiam, nenhuma pessoa disse:’ Vamos sentar e organizar um corpo coerente de matemática que representa uma educação de graduação ‘”, disse Buzzard. “Estamos fazendo algo que vai entender as questões em um exame final de graduação, e isso nunca foi feito antes.”
Provavelmente levará décadas antes que mathlib tenha o conteúdo de uma biblioteca de pesquisa real, mas os usuários Lean mostraram que um catálogo tão abrangente é pelo menos possível – que chegar lá é apenas uma questão de programação em toda a matemática.
Para tanto, no ano passado Buzzard, Massot e Johan Commelin, da Universidade de Friburgo, na Alemanha, empreenderam um ambicioso projeto de prova de conceito. Eles colocaram temporariamente de lado o acúmulo gradual de matemática na graduação e pularam para a vanguarda do campo. O objetivo era definir uma das grandes inovações da matemática do século 21 – um objeto chamado espaço perfectoide que foi desenvolvido na última década por Peter Scholze, da Universidade de Bonn. Em 2018, o trabalho rendeu a Medalha Scholze the Fields, a maior homenagem da matemática.
Buzzard, Massot e Commelin esperavam demonstrar que, pelo menos em princípio, Lean pode lidar com o tipo de matemática com que os matemáticos realmente se importam. “Eles estão pegando algo muito sofisticado e recente e mostrando que é possível trabalhar nesses objetos com um assistente de prova”, disse Mahboubi.
Para definir um espaço perfectoide, os três matemáticos tiveram que combinar mais de 3.000 definições de outros objetos matemáticos e 30.000 conexões entre eles. As definições se espalharam por muitas áreas da matemática, da álgebra à topologia à geometria. A maneira como eles se juntaram na definição de um único objeto é uma ilustração vívida de como a matemática fica mais complexa ao longo do tempo – e de por que é tão importante estabelecer as bases da matemática corretamente.
“Muitos campos da matemática avançada exigem todo tipo de matemática que você aprende na graduação”, disse Macbeth.
O trio conseguiu definir um espaço perfectoide, mas pelo menos por agora, os matemáticos não podem fazer muito com ele. O Lean precisa de acesso a muito mais matemática antes mesmo de formular os tipos de questões sofisticadas nas quais surgem os espaços perfetóides.
“É um pouco ridículo que Lean saiba o que é um espaço perfectoide, mas não conheça análises complexas”, disse Massot.
Buzzard concorda, chamando a formalização de espaços perfetóides de “truque” – o tipo de proeza inicial que as novas tecnologias às vezes realizam para demonstrar seu valor. Nesse caso, funcionou.
“Você não deve pensar que, por causa de nosso trabalho, todos os matemáticos da Terra começaram a usar um assistente de prova”, disse Massot, “mas acho que muitos deles notaram e fizeram muitas perguntas”.
Ainda vai demorar muito até que o Lean seja uma parte real da pesquisa matemática. Mas isso não significa que o programa seja um espetáculo secundário de ficção científica hoje. Os matemáticos ocupados em desenvolvê-lo vêem seu trabalho como semelhante ao de colocar os primeiros trilhos de ferrovia – um começo necessário para um empreendimento importante, mesmo que eles próprios nunca possam dar uma volta.
“Será tão legal que valerá a pena um grande investimento agora”, disse Macbeth. “Estou investindo tempo agora para que alguém no futuro possa ter essa experiência incrível.”
Publicado em 03/10/2020 18h28
Artigo original:
Achou importante? Compartilhe!
Assine nossa newsletter e fique informado sobre Astrofísica, Biofísica, Geofísica e outras áreas. Preencha seu e-mail no espaço abaixo e clique em “OK”: