Uma pequena comunidade de matemáticos está usando o Lean para construir uma nova base digital. Eles esperam que isso garanta o futuro de seu campo científico.
Todos os dias, dezenas de matemáticos com ideias semelhantes se encontram no chat Zulip para trabalhar no que acreditam moldar o futuro de seu campo científico.
Todos são fãs do programa Lean . É uma ferramenta interativa de prova de teorema que, em princípio, é capaz de ajudar matemáticos a escrever provas. No entanto, para isso, os matemáticos devem inserir manualmente as regras matemáticas na base do programa, trazendo o conhecimento coletado ao longo de milhares de anos para uma forma que um computador possa entender.
Para muitos participantes do projeto, seus benefícios requerem pouca ou nenhuma explicação.
“Em um nível fundamental, é óbvio que uma vez que algo é digitalizado, ele pode ser usado de novas maneiras”, disse Kevin Buzzarddo Imperial College London. "E vamos digitalizar a matemática, tornando-a melhor."
Digitalizar matemática é um sonho antigo. Os benefícios esperados vão desde o trivial - verificar os trabalhos de casa dos alunos com computadores - ao extraordinário: usar a inteligência artificial para fazer novas descobertas matemáticas e encontrar novas soluções para velhos problemas. Os matemáticos acreditam que os provadores automáticos de teoremas também serão capazes de revisar artigos submetidos a periódicos, encontrar erros que os revisores humanos às vezes não percebem e se envolver no tedioso trabalho técnico de preencher a prova com todos os detalhes necessários.
Mas, primeiro, os matemáticos reunidos em um bate-papo precisam equipar o Lean com conhecimentos no âmbito da matemática escolar e, até agora, essa tarefa está apenas pela metade. Em um futuro próximo, é improvável que o Lean seja capaz de resolver problemas em aberto, mas as pessoas que trabalham na base têm quase certeza de que em apenas alguns anos o programa pelo menos aprenderá a entender questões de nível de exame no ensino médio.
Quem sabe? Os matemáticos que participam do projeto nem sempre têm uma ideia clara de para que a matemática digital pode ser útil.
“Não sabemos exatamente para onde estamos indo”, disse Sebastien Gösel, da Universidade de Rennes.
Você planeja, o Lean funciona
No verão, um grupo de usuários avançados de Lean realizou um seminário online " Lean para Matemáticos Curiosos ". Na primeira lição, Scott Morrison, da University of Sydney, mostrou como você pode escrever uma prova usando um programa.
Ele começou escrevendo a declaração que queria provar em termos Lean. Na linguagem humana, significava "há um número infinito de números primos". Existem várias maneiras de provar essa afirmação, mas Morrison queria usar uma versão ligeiramente modificada da primeira evidência encontrada por Euclides em 300 aC. Na prova, todos os números primos conhecidos são multiplicados e, depois de somar 1, um novo número primo é obtido (o próprio produto ou um de seus divisores será primo). A escolha de Morrison baseou-se em uma das regras básicas para o uso do Lean: o próprio usuário deve ter a ideia principal da prova.
"Você é responsável pelo primeiro palpite", disse Morrison em uma entrevista.
Depois de entrar na afirmação e escolher uma estratégia, Morrison esboçou a estrutura da prova em alguns minutos. Ele identificou uma sequência de etapas intermediárias, cada uma das quais era relativamente fácil de provar. Embora o Lean não possa oferecer uma estratégia de prova geral, ele pode ajudá-lo a executar etapas pequenas e concretas. Dividindo a prova em subtarefas acessíveis, Morrison era um pouco como um chef instruindo chefs regulares para cortar cebolas ou ferver água. “É aqui que você espera que o Lean assuma o controle e o ajude”, disse Morrison.
O Lean realiza tarefas intermediárias usando processos automatizados chamados táticas. Esses são algoritmos curtos projetados para realizar tarefas muito específicas.
Trabalhando com provas, Morrison lançou uma tática chamada pesquisa de biblioteca. Ela vasculhou o banco de dados matemático do programa e retornou vários teoremas que ela pensou que poderiam preencher as lacunas em uma seção específica da prova. Diferentes táticas executam diferentes tarefas matemáticas. Um deles, linarith, pode tomar um conjunto de desigualdades para, digamos, dois números reais e confirmar a verdade da nova desigualdade, que inclui o terceiro número: se a é 2 e b é maior que a, então 3a + 4b é maior que 12. O outro faz a maior parte trabalhar com regras algébricas básicas, como associatividade.
“Dois anos atrás, no Lean, a associatividade tinha que ser aplicada manualmente”, disse Amelia Livingston, uma estudante de matemática no Imperial College London que está estudando Lean com Buzzard. - E então alguém escreveu uma tática que faz isso por você. Fico feliz sempre que o uso. "
Ao todo, Morrison levou 20 minutos para concluir a prova de Euclides. Aqui e ali, ele mesmo completou os detalhes; às vezes os estrategistas faziam isso por ele. Após cada etapa, Lean verificou a consistência da prova em relação às regras lógicas integradas escritas em uma linguagem formal chamada teoria de tipo dependente .
“Parece um aplicativo Sudoku. Se você fizer um movimento errado, ele apita ”, disse Buzzard. Como resultado, Lean confirmou a viabilidade da prova de Morrison.
Foi um exercício muito divertido - como normalmente é o caso quando a tecnologia faz algo por você. No entanto, a prova de Euclides existe há mais de 2.000 anos. As questões dos matemáticos de hoje são tão complexas que Lean ainda não consegue entender as questões, muito menos ajudar a respondê-las.
“Provavelmente levará décadas para que essa ferramenta ajude na pesquisa”, disse Heather Macbeth, da Fordham University, uma das usuárias do Lean.
Portanto, antes que os matemáticos possam trabalhar com o Lean em questões que sejam realmente interessantes para eles, eles precisam adicionar mais regras matemáticas ao programa. E esta, de fato, é uma tarefa bastante simples.
Anatomia de um programa de construção de provas: o Lean ajuda os matemáticos a provar teoremas ao verificar o trabalho e automatizar algumas das etapas nas provas.
1) O matemático descreve a estrutura básica da prova e escreve a sequência de passos em Lean.
2) A biblioteca mathlib de programas matemáticos possui um conjunto de táticas que executam as etapas desta prova. Os matemáticos continuam adicionando novos dados ao mathlib. Teoremas comprovados são adicionados ao mathlib.
3) O algoritmo do Kernel verifica a exatidão da prova usando regras simples.
* O polvo tornou-se, de alguma forma, a designação de emoções alegres na comunidade Lean.
“Para que o Lean entenda algo, as pessoas precisam traduzir os livros didáticos de matemática de uma forma que o programa possa entender”, disse Morrison.
Infelizmente, a simplicidade de um problema não significa que seja fácil de concluir - visto que grande parte da matemática não é abordada nos livros didáticos.
Conhecimento disperso
Se você não estudou matemática avançada, esta área pode parecer precisa e bem descrita para você. Álgebra, cálculo diferencial, análise matemática - tudo resulta de tudo, e há respostas para todas as perguntas, listadas no final do livro.
No entanto, a matemática no currículo escolar, no currículo da faculdade e até mesmo em grande parte da universidade é uma parte cada vez menor de todo o conhecimento. A maioria deles não é bem organizada.
Existem áreas enormes e importantes da matemática que não estão totalmente descritas. Eles estão armazenados na cabeça de um pequeno número de pessoas que aprenderam seu subcampo da matemática com outras pessoas, aprenderam com aqueles que os inventaram - isto é, eles existem com base no folclore.
Existem outras áreas onde o material básico foi escrito, mas é tão complexo e longo que ninguém foi capaz de verificar se está correto. Em vez disso, os matemáticos simplesmente acreditam nele.
“Contamos com a reputação do autor. Sabemos que ele é um gênio e um cara meticuloso, então a prova provavelmente é verdadeira ”, disse Patrick Massot, da Universidade de Paris-Saclay.
Esta é uma das razões pelas quais os programas de prova de teoremas são tão atraentes. Traduzir a matemática em uma linguagem compreensível por um computador força os matemáticos a finalmente catalogar seu conhecimento e definir com precisão todos os objetos.
Assia Mabubido Instituto Estatal Francês de Pesquisa em Informática e Automação relembra a primeira vez que percebeu o potencial de uma biblioteca digital tão ordenada: “Fiquei fascinada com a possibilidade de cobertura teórica de toda a literatura matemática usando a linguagem da lógica pura, armazenando toda a biblioteca matemática em um computador, verificando e procurando dados nela com a ajuda de programas ".
Lean não é o primeiro programa a ter esse potencial. O primeiro, Automath, apareceu na década de 1960, e Coq, um dos mais populares hoje, foi lançado em 1989. Os usuários do Coq formalizaram muita matemática em linguagem de programa, mas esse trabalho era descentralizado e não bem organizado. Os matemáticos trabalharam apenas em projetos de seu interesse e identificaram apenas os objetos de que precisavam para seu próprio trabalho, muitas vezes descrevendo-os de maneiras únicas. Como resultado, as bibliotecas de Coq parecem desordenadas, como um projeto para uma cidade que cresceu naturalmente.
“Coq é um velho com cicatrizes hoje”, disse Mabubi, que tem participado do programa. "Ele foi apoiado por muitas pessoas por muito tempo e, graças à sua longa história, suas deficiências agora são bem conhecidas."
Em 2013, Leonardo de Mura , pesquisador da Microsoft, lançou o projeto Lean. Seu nome [lean] reflete o desejo de Moore de criar um programa eficiente e limpo. Ele presumiu que o programa seria uma ferramenta para verificar a precisão do código de outros programas, não a matemática. No entanto, verifica-se que verificar a exatidão de um programa é muito parecido com verificar uma prova.
“Nós criamos o Lean porque estamos interessados no desenvolvimento de software e existe uma analogia entre criar matemática e escrever código”, disse de Moore.
Heather Macbeth da Fordham University, uma das usuárias do Lean
Na época do lançamento do Lean, havia alguns outros programas auxiliares, incluindo o Coq, que é mais semelhante ao Lean. A base lógica para ambos os programas é baseada na teoria dos tipos dependentes. No entanto, o Lean oferece uma chance de recomeçar.
Ela rapidamente atraiu matemáticos. Eles o usaram com tanto entusiasmo que começaram a ocupar todo o tempo livre de De Moore com suas questões sobre o desenvolvimento no campo da matemática. "Ele ficou um pouco cansado de matemáticos importantes e disse - por que vocês não fazem um repositório separado?" Morrison disse.
Os matemáticos criaram esta biblioteca em 2017. Eles o chamaram de mathlib e zelosamente começaram a preenchê-lo com o conhecimento matemático mundial, criando algo como um análogo da Biblioteca de Alexandria.no século XXI. Os matemáticos criaram e carregaram fragmentos de matemática digitalizada, criando gradualmente um catálogo para o Lean. E, como o mathlib era novo, eles podiam aprender com as limitações de sistemas anteriores, como o Coq, e controlar como o material era organizado.
“Há uma tentativa deliberada de criar uma biblioteca matemática monolítica, cujos fragmentos funcionarão uns com os outros”, disse Macbeth.
Mathlib alexandrino
A página inicial do projeto mathlib possui gráficos que mostram o andamento do projeto em tempo real. O projeto tem uma lista dos líderes que mais investem nele, ordenados pelo número de linhas de código [em primeiro lugar, aliás, é o matemático russo Yuri Kudryashov / aprox. trad.]. O número total de objetos matemáticos digitalizados também é calculado: no início de outubro, ele contém 18.756 definições e 39.157 teoremas.
Todos esses ingredientes da matemática podem ser combinados para criar matemática dentro do Lean. Até agora, seu sortimento é severamente limitado, apesar dos números aparentemente impressionantes. Não há quase nada de áreas de análise complexa ou equações diferenciais - e esses são dois elementos básicos de muitas áreas da matemática superior. Além disso, o programa ainda não sabe o suficiente para sequer descrever qualquer um dos Problemas do Milênio - problemas matemáticos definidos pelo Clay Mathematical Institute em 2000 como "problemas clássicos importantes que não foram resolvidos por muitos anos."
mathlib está lenta mas seguramente preenchendo. O trabalho prossegue em espírito de equipe. No chat Zulip, os matemáticos selecionam as definições para formalizar, são desafiados a escrevê-las e fornecer feedback imediato sobre o trabalho dos outros.
“Qualquer matemático pesquisador pode estudar mathlib e fazer uma lista de 40 coisas que não estão lá”, disse Macbeth. - Então ele decide preencher qualquer uma dessas lacunas. E o prazer instantâneo é garantido - alguém lerá seu trabalho e deixará um comentário sobre ele em 24 horas. "
Muitos complementos saem pequenos - como Sophie Morel descobriuda Escola Normal de Lyon durante o seminário online "Lean for Curious Mathematicians". Os organizadores da conferência deram aos participantes afirmações matemáticas relativamente simples para serem comprovadas no Lean como prática. Trabalhando com um deles, Morel percebeu que sua prova exigia um lema - um pequeno resultado intermediário - que não foi encontrado em mathlib.
“Foi um pedacinho da álgebra linear que, por algum motivo, ainda não estava lá. As pessoas que preenchem a lib matemática tentam entender tudo, mas você não pode prever todas as opções ”, disse Morel, que inseriu o lema obrigatório três linhas na base.
Outras contribuições são mais significativas. No ano passado, Gösel tem trabalhado na definição de um manifold suave para mathlib. Variedades suaves são conjuntos (como linhas, círculos ou superfícies de uma bola) que desempenham um papel fundamental no estudo da geometria e da topologia. Eles também costumam desempenhar um papel importante em problemas de áreas como teoria dos números e cálculo. A maioria das pesquisas matemáticas é impossível sem eles.
No entanto, variedades suaves podem se ocultar sob diferentes disfarces - tudo depende do contexto. Eles podem ter um número finito ou infinito de dimensões, ter limites ou não, ser definidos em vários sistemas numéricos - no conjunto de real, complexo ou p-ádiconúmeros. Definir a diversidade uniforme é como definir o amor: você o reconhece quando o encontra, mas qualquer definição estrita certamente deixará de lado alguns dos exemplos mais óbvios desse fenômeno.
“Ao definir as coisas básicas, você não precisa fazer nenhuma escolha”, disse Gösel. "Mas objetos mais complexos podem ser formalizados de 10 a 20 maneiras diferentes."
Gösel precisa manter um equilíbrio entre especificidade e generalização. “Eu tinha uma regra - queria ser capaz de definir 15 usos diferentes de manifolds”, disse ele. “Ao mesmo tempo, não queria que a definição fosse muito geral, caso contrário, seria impossível trabalhar com ela.”
A definição que ele desenvolveu se encaixa em 1.600 linhas de código - bastante para uma definição de mathlib, mas talvez não tanto em comparação com todas as possibilidades matemáticas que ele abre para o Lean.
“Agora que temos a linguagem de que precisamos, podemos começar a provar teoremas”, disse ele.
Encontrar a definição correta de um objeto do grau correto de generalidade é a principal ocupação dos matemáticos que preenchem o mathlib. Os criadores da biblioteca esperam definir objetos de uma forma que seja útil hoje e, ao mesmo tempo, flexível o suficiente para que esses objetos possam ser usados de uma forma que é imprevisível hoje.
“A necessidade de que tudo seja útil para uso no futuro distante é sublinhada”, disse Macbeth.
Os perfectoides nascem da prática
Mas o Lean não é apenas uma ferramenta útil - dá aos matemáticos a chance de retomar seu trabalho. Macbeth ainda se lembra da primeira vez em que tentou um programa para ajudar a escrever provas. Era 2019 e o programa era Coq (embora agora tenha mudado para Lean). Ela não conseguia parar.
“Em um fim de semana louco, trabalhei com este programa por 12 horas seguidas”, disse ela. "Era um verdadeiro vício."
Outros matemáticos descrevem suas experiências de maneira semelhante. Lean, dizem eles, é como um jogo de computador - reduzido aos mesmos hormônios de recompensa que tornam difícil deixar o controle do jogo de lado. “Você pode fazer isso 14 horas por dia sem se sentir cansado e em um estado elevado o dia todo”, disse Livingston. "Você recebe feedback positivo o tempo todo."
Sebastien Gösel
Ainda assim, a comunidade Lean entende que, para muitos matemáticos, simplesmente não há níveis suficientes em seu programa.
"Se você quantificar a porcentagem de matemática formalizada, diria que menos de um milésimo de um por cento ainda está pronto", disse Christian Szegedi, um programador do Google que trabalha em sistemas de IA que sonha em ser capaz de ler e formalizar de forma independente livros didáticos de matemática.
Mas os matemáticos estão aumentando essa porcentagem. Se hoje o mathlib contém a maior parte do material ensinado por alunos do segundo ano da universidade, os participantes do projeto esperam adicionar o restante do programa em alguns anos - e isso será uma conquista significativa.
“Em todos os 50 anos desses sistemas, ninguém sugeriu: vamos sentar e organizar uma base de conhecimento consistente de matemática, descrevendo o material do instituto”, disse Buzzard. "Estamos criando algo que pode entender as questões do exame do instituto - isso não acontecia antes."
Provavelmente, levarão décadas até que o conteúdo da mathlib corresponda à biblioteca de pesquisa, mas os usuários Lean demonstram pelo menos a possibilidade teórica de criar tal catálogo - e atingir esse objetivo simplesmente depende de inserir toda a matemática no banco de dados na forma de código do programa.
Para isso, no ano passado Buzzard, Masso e Johan Kommelin da Universidade de Friburgo, na Alemanha, implementaram um projeto que prova a viabilidade desse sonho. Eles adiaram temporariamente o enchimento gradual da base com o material do instituto e seguiram para áreas avançadas. O objetivo era identificar uma das maiores inovações em matemática do século 21 - um objeto como o "espaço perfectoide" desenvolvido nos últimos dez anos por Peter Scholze, da Universidade de Bonn. Em 2018, recebeu o Prêmio Fields por seu trabalho, o maior prêmio da matemática.
Buzzard, Masso e Commelin queriam demonstrar que, pelo menos em princípio, Lean pode trabalhar com matemática em que os matemáticos estão realmente interessados. “Eles pegaram algo muito complexo e novo e mostraram que esses objetos podem ser manipulados com um programa para ajudar a escrever provas”, disse Mabubi.
Kevin Buzzard
Para definir um espaço perfectoide, três matemáticos precisaram combinar mais de 3.000 definições de objetos matemáticos e 30.000 conexões entre eles. As definições se estenderam por muitas áreas da matemática, da álgebra à topologia e geometria. Colocá-los juntos em uma definição foi uma demonstração poderosa do crescimento da complexidade da matemática ao longo do tempo - e por que é tão importante obter as bases certas para a matemática.
“Muitas áreas da matemática avançada exigem que você conheça todos os tipos de matemática que são ensinados aos alunos”, disse Macbeth.
O Trinity conseguiu definir o espaço perfectoide, mas até agora há pouco que os matemáticos possam fazer com ele. Muitas outras definições matemáticas precisam ser introduzidas no Lean antes que o programa possa pelo menos formular aquelas questões complexas nas quais surgem esses espaços perfeitos.
“É muito bobo que Lean saiba o que é um espaço perfectoide, mas não conheça análises complexas”, disse Masso.
Buzzard concorda, chamando a formalização do espaço perfectoide de "truque" - um truque que as novas tecnologias às vezes mostram para demonstrar sua utilidade. E desta vez o truque funcionou.
“Você não precisa pensar que, graças ao nosso trabalho, todos os matemáticos da Terra começaram a usar programas para ajudar a escrever provas”, disse Masso, “mas acho que muitos deles perceberam essa possibilidade e começaram a fazer perguntas”.
Levará muito tempo até que o Lean possa se tornar uma parte real da pesquisa matemática. No entanto, isso não significa que o programa hoje seja uma imagem de ficção científica. Os matemáticos envolvidos em seu desenvolvimento comparam seu trabalho com a construção dos primeiros trilhos - o início necessário de um empreendimento importante, mesmo que eles próprios não sejam capazes de percorrer os trilhos.
“Vai ser uma coisa tão legal que vale a pena o trabalho de hoje”, disse Macbeth. "Estou investindo meu tempo nela hoje para que alguém no futuro possa ter uma experiência incrível trabalhando com ela."