Considerando os tópicos abordados em uma conferência como a STOC, existem pesquisadores de algoritmo ou complexidade usando ativamente o COQ ou Isabelle? Se sim, como eles estão usando isso em suas pesquisas? Suponho que a maioria das pessoas não usaria essas ferramentas porque as provas seriam de nível muito baixo. Alguém está usando esses assistentes de prova de uma maneira crítica para sua pesquisa, em vez de um bom complemento?
Estou interessado porque posso começar a aprender uma dessas ferramentas e seria divertido aprender sobre elas no contexto de provas de reduções, correção ou tempo de execução.
Respostas:
Uma regra geral é que, quanto mais abstrata / exótica for a matemática que você deseja mecanizar, mais fácil será. Por outro lado, quanto mais concreta / familiar for a matemática, mais difícil será. Portanto (por exemplo) animais raros, como topologia sem pontos predicativos, são muito mais fáceis de mecanizar do que a topologia métrica comum.
Inicialmente, isso pode parecer um pouco surpreendente, mas isso ocorre basicamente porque objetos concretos, como números reais, participam de uma variedade selvagem de estruturas algébricas, e as provas que os envolvem podem fazer uso de qualquer propriedade de qualquer visualização delas. Portanto, para poder entender o raciocínio comum a que os matemáticos estão acostumados, é necessário mecanizar todas essas coisas. Por outro lado, construções altamente abstratas têm um conjunto (deliberadamente) pequeno e restrito de propriedades; portanto, você precisa mecanizar muito menos antes de obter os bons bits.
Provas na teoria da complexidade e algoritmos / estruturas de dados tendem (via regra) a usar propriedades sofisticadas de dispositivos simples como números, árvores ou listas. Por exemplo, argumentos combinatórios, probabilísticos e teóricos dos números rotineiramente aparecem todos ao mesmo tempo em teoremas da teoria da complexidade. Obter suporte à biblioteca assistente de provas até o ponto em que isso é bom de fazer é bastante trabalho!
Um contexto em que as pessoas estão dispostas a colocar o trabalho é em algoritmos criptográficos. Existem restrições algorítmicas muito sutis por razões matemáticas complexas e, como o código criptográfico é executado em um ambiente adversário, até o menor erro pode ser desastroso. Por exemplo, o projeto Certicrypt construiu muita infraestrutura de verificação com o objetivo de criar provas verificadas por máquina da exatidão dos algoritmos criptográficos.
fonte
Um exemplo muito importante é a formalização de Gonthiers Coq do teorema das 4 cores em Coq, que utiliza muita combinação.
Meu colega Uli Schöpp usou a biblioteca ssreflect desenvolvida por Gonthier para esse fim, a fim de verificar (e estender um pouco) também no Coq um resultado de Cook e Rackoff em autômatos gráficos. https://scholar.google.at/scholar?oi=bibs&cluster=4944920843669159892&btnI=1&hl=de (Schöpp, U. (2008). Um limite inferior formalizado para a acessibilidade de gráficos não direcionados. Em lógica para programação, inteligência artificial e raciocínio 621-635). Springer Berlin / Heidelberg.)
fonte