O projeto de teorias equacionais: um breve passeio

Há quase três semanas, eu propôs um projeto colaborativocombinando os esforços de matemáticos profissionais e amadores, provadores automáticos de teoremas, ferramentas de IA e a linguagem assistente de prova Lean, para descrever o gráfico de implicação relacionando o 4694 leis equacionais para magmas que pode ser expresso usando até quatro invocações da operação magma. Ou seja, é preciso determinar a verdade ou falsidade do possíveis implicações entre essas 4.694 leis.

O projeto foi lançado no dia da postagem no weblog, e está em funcionamento há 19 dias agitados até agora; ver meu registro pessoal do projeto para um resumo diário dos eventos. Do ponto de vista das implicações brutas resolvidas, o projeto está (no momento em que este artigo foi escrito) 99,9963% concluído: do implicações para resolver, foram provados como verdadeiros, provaram ser falsas, e apenas permanecem abertos, embora mesmo dentro deste conjunto, existam implicações que conjecturamos serem falsas e que provavelmente seremos capazes de refutar formalmente em breve. Por razões de eficiência de compilação, não registramos a prova de cada uma dessas afirmações no Lean; provamos apenas um conjunto menor de implicações no Lean, que então implicam o conjunto mais amplo de implicações através da transitividade (por exemplo, usando o fato de que se a Equação implica equação e equação implica equação então Equação implica equação ); em breve também implementaremos uma redução adicional utilizando uma simetria de dualidade do gráfico de implicação.

Graças aos esforços incansáveis ​​de muitos colaboradores voluntários para o projetoagora temos uma série de ótimas ferramentas de visualização para inspecionar várias partes do gráfico de implicação (não totalmente concluído). Por exemplo, este gráfico descreve todas as consequências Equação 1491: que apelidei de “Lei Obélix”(e tem um companheiro, o“Lei Astérix“, Equação 65: ). E aqui está um tabela de todas as leis equacionais estamos estudando, juntamente com uma contagem de quantas leis elas implicam ou estão implícitas. Essas interfaces também estão um pouco integradas com o Lean: por exemplo, você pode Clique aqui tentar mostrar que a lei Obelix implica Equação 359, ; Vou deixar isso como um desafio (é possível uma prova de quatro linhas no Lean).

Nas últimas semanas, aprendi que muitas dessas leis já apareceram na literatura e compilei um “tour” por essas equações aqui. Por exemplo, além da muito conhecida lei comutativa (Equação 43) e direito associativo (Equação 4512), algumas equações (Equação 14, Equação 29, Equação 381, Equação 3722e Equação 3744) apareceu em algumas competições de matemática de Putnam; Equação 168 outline uma estrutura fascinante, conhecida como “grupóide central”, que foi estudada em specific por Evans e por Knuthe foi uma inspiração elementary para o Algoritmo de conclusão Knuth-Bendix; e Equação 1571 classifica grupos abelianos de expoente dois.

Graças ao Teorema da completude de Birkhoffse uma lei equacional implica outra, então ela pode ser provada por um número finito de operações de reescrita; no entanto, o número de reescritas necessárias pode ser bastante demorado. A implicação de 359 de 1491 mencionada acima já é moderadamente desafiadora, exigindo quatro ou cinco reescritas; a implicação da Equação 2 de Equação 1689 é incrivelmente longo (experimente!). No entanto, provadores de teoremas automatizados padrão, como Vampirosão perfeitamente capazes de provar a grande maioria dessas implicações.

Mais sutis são os anti-implicaçõesem que temos que mostrar que uma lei não implica uma lei . Em princípio, basta exibir um magma que obedeça mas não . Numa grande fração de casos, pode-se simplesmente pesquisar pequenos magmas finitos – como magmas de dois, três ou quatro elementos – para obter esta anti-implicação; mas nem sempre são suficientes e, de facto, conhecemos anti-implicações que só podem ser comprovadas através da construção de um magma infinito. Por exemplo, a “lei Asterix” é agora conhecida (a partir dos esforços deste projecto) por não implica a “lei Obelix”, mas todos os contra-exemplos são necessariamente infinitos. Curiosamente, as construções conhecidas têm alguma afinidade com a famosa técnica de forçando na teoria dos conjuntos, na medida em que adicionamos continuamente elementos “genéricos” a um magma (parcial) a fim de forçar a existência de um contraexemplo com certas propriedades especificadas, embora as construções aqui sejam certamente muito mais simples do que nas construções da teoria dos conjuntos.

Também obtivemos lucro lucrativo com construções de magmas “lineares” em anéis comutativos e não comutativos; magmas livres associados a “confluente”leis equacionais e, mais geralmente, leis com completa sistemas de reescrita. Como tal, o número de implicações não resolvidas continua a diminuir a um ritmo constante, embora ainda não estejamos prontos para declarar vitória no projecto.

Depois de uma quantidade bastante agitada de configuração de back-end e “apagamento de incêndios”, o projeto agora está funcionando razoavelmente bem, com atividades coordenadas em um Canal Lean Zulipe todas as contribuições que passam por um processo de solicitação pull no Github e são rastreadas por meio de um projeto Github baseado em problemas com a supervisão inestimável fornecida pelos outros dois mantenedores do projeto, Pietro Monticone e Shreyas Srinivas. Em contraste com o anterior Projeto de formalização do PFRo fluxo de trabalho segue as práticas padrão do Github e procede aproximadamente da seguinte forma: se, durante o curso da discussão do Zulip, ficar claro que alguma tarefa específica precisa ser realizada para levar o projeto adiante (por exemplo, formalizar em Lean a prova de um implicação que foi trabalhada nos tópicos de discussão), um “problema” é criado (muitas vezes por mim mesmo ou por um dos outros mantenedores), que outros contribuidores podem então “reivindicar”, trabalhar separadamente (usando uma cópia native do arquivo principal). Repositório Github) e, em seguida, envie uma “solicitação pull” para mesclar sua contribuição de volta ao repositório principal. Esta solicitação pode então ser revisada tanto pelos mantenedores quanto por outros contribuidores e, se aprovada, encerra o problema relevante.

De forma mais geral, estamos tentando documentar todos os processos e lições aprendidas com esta configuração, e isso fará parte de um próximo documento sobre este projeto, que estamos agora no etapas preliminares do planejamentoe provavelmente incluirá dezenas de autores.

Embora o projecto ainda esteja em curso, posso dizer que estou bastante satisfeito com o progresso alcançado até à information e que muitas das minhas esperanças relativamente a um projecto deste tipo já se concretizaram. Do lado científico, descobrimos algumas novas técnicas e construções para mostrar que uma dada teoria equacional não implica outra, e também descobrimos algumas estruturas algébricas exóticas, como o par “Asterix” e “Obelix”, que têm interessantes características, e que provavelmente não teriam sido descobertas por qualquer outro meio que não o tipo de pesquisa sistemática conduzida aqui. Os participantes são muito diversos, desde matemáticos e cientistas da computação em todos os estágios de carreira, até estudantes interessados ​​e amadores. A plataforma Lean funcionou bem na integração de contribuições geradas por humanos e por máquinas; estes últimos são numericamente, de longe, a maior fonte de contribuições, mas muitos dos resultados gerados automaticamente foram obtidos primeiro em casos especiais por seres humanos e depois generalizados e formalizados (muitas vezes por diferentes membros do projeto). Ainda apresentamos muitos argumentos matemáticos informais no tópico de discussão, mas eles tendem a ser rapidamente formalizados em Lean, altura em que as disputas sobre a correcção desaparecem, e podemos, em vez disso, concentrar-nos na melhor forma de implementar várias técnicas verificadas para lidar com as implicações restantes.

Talvez a única coisa que eu esperava ver neste momento e que ainda não se concretizou sejam contribuições significativas de ferramentas modernas de IA. Eles estão sendo usados ​​de várias maneiras secundárias neste projeto, por exemplo, através de ferramentas como o copiloto do Github para acelerar a escrita de provas Lean, o Projeto LaTeXe outros códigos de software program, e várias de nossas ferramentas de visualização também foram amplamente co-escritas usando grandes modelos de linguagem, como Claude. No entanto, para a tarefa central de resolver implicações, os provadores automatizados de teoremas, mais “antiquados”, têm se mostrado superiores até agora. No entanto, a maioria das cerca de 700 implicações restantes não são passíveis de utilização destas ferramentas mais antigas, e várias (particularmente as que envolvem “Asterix” e “Obelix” bloquearam os colaboradores humanos durante vários dias), por isso ainda posso ver um papel para a IA moderna desempenhe um papel mais ativo na eliminação das implicações mais difíceis e teimosas restantes.