• Fernando Giannini

Construindo a Biblioteca Matemática do Futuro

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.

Fonte: bakaarts https://www.instagram.com/bakaarts/


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 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, ao digitalizar algo, você 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 a matemática é um sonho antigo. Os benefícios esperados vão dos computadores mundanos, dando notas aos deveres de casa dos estudantes - 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 possa revisar as submissões de periódicos, encontrando erros que as revisões humanas 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 ao 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 curtas


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ê é o 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 dividir a prova em subtarefas gerenciáveis, Morrison era um pouco como um chef instruindo cozinheiros numa linha de cortar 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 do 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 de "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 3 a + 4 b é 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 completar 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, o Lean verificava 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, ele irá avisar ”, 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 o 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.

“O Lean deve ser capaz de entender algo, é basicamente uma questão dos seres humanos terem [livros de matemática traduzidos] na forma que o Lean pode entender”, disse Morrison.


Infelizmente, não significa ser uma tarefa fácil, especialmente considerando que, para grande parte da matemática, os livros didáticos realmente não existem.


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, no gabarito e 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 a aprenderam com a pessoa que a inventou - ou seja, ela 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 ele 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.


Construímos o Lean porque nos preocupamos com o desenvolvimento de software, e existe uma analogia entre construir matemática e construir software. Leonardo de Moura, Microsoft Research

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 armazenar em um computador que verifique a lógica 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 amplamente usados ​​hoje, saiu 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 há uma analogia entre construir matemática e construir software”, disse de Moura.

Heather Macbeth, uma matemática da Fordham University, diz que assistentes de prova como Lean não são apenas úteis, eles são quase viciantes.


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 migraram para ele rapidamente. Eles adotaram o programa com tanto entusiasmo que começaram a consumir o tempo 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.


Os 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 esforço real 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 colaboradores, 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.740 definições e 39.020 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 se 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. No 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ão 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 o mathlib não tinha.


“Era uma coisa muito pequena sobre á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.


Ele também costuma 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.


"Qualquer matemático pesquisador pode olhar para mathlib e ver 40 coisas que está faltando. Então você decide preencher um desses buracos. É realmente uma gratificação instantânea". Heather Macbeth, Fordham University

Mas as variedades suaves vêm em diferentes formas, dependendo do contexto. Eles podem ser de dimensão finita ou dimensão infinita, ter “limite” ou não ter limite 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: conheço 15 aplicações de manifolds que 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 tudo ser útil em um futuro distante”, disse Macbeth.


Só a prática traz a perfeição


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."

Enquanto Sébastien Gouëzel trabalhava na definição de um “manifold suave” para mathlib, ele teve que equilibrar especificidade com flexibilidade. (Cortesia de Sebastian Gouezel


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 existiram, 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.

Kevin Buzzard ajudou a escrever uma definição digital de um dos maiores e mais complicados objetos matemáticos do século 21: o espaço perfetóide.


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 mathlib 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 enquanto, 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 deveria 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 vale 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.”


Artigo: Kevin Hartnett

Fonte: https://www.quantamagazine.org/building-the-mathematical-library-of-the-future-20201001/










Receba as notícias sobre educação e tecnologia 

Fernando Giannini

 

E-mail:

fernando.giannini@streamer.com.br

logo-3.png

© 2020 por Fernando Giannini