Prueba de uso del asistente en la investigación de la teoría de la complejidad?

Teniendo en cuenta los temas tratados en una conferencia como STOC, ¿hay algún algoritmo o investigador de complejidad que use activamente COQ o Isabelle? Si es así, ¿cómo lo usan en su investigación? Supongo que la mayoría de la gente no usaría tales herramientas porque las pruebas serían de un nivel demasiado bajo. ¿Alguien está utilizando estos asistentes de prueba de una manera crítica para su investigación, en lugar de un buen suplemento?

Estoy interesado porque podría comenzar a aprender una de esas herramientas y sería divertido aprender sobre ellas en el contexto de pruebas de reducciones, corrección o tiempo de ejecución.

Una regla general es que cuanto más abstractas / exóticas sean las matemáticas que desea mecanizar, más fácil será. Por el contrario, cuanto más concretas / familiares sean las matemáticas, más difícil será. Entonces (por ejemplo) los animales raros como la topología libre de puntos predicativos son mucho más fáciles de mecanizar que la topología métrica ordinaria.

Inicialmente, esto puede parecer un poco sorprendente, pero esto se debe básicamente a que los objetos concretos como los números reales participan en una gran variedad de estructuras algebraicas, y las pruebas que los involucran pueden hacer uso de cualquier propiedad desde cualquier punto de vista. Entonces, para poder utilizar el razonamiento ordinario al que están acostumbrados los matemáticos, debes mecanizar todas estas cosas. Por el contrario, las construcciones altamente abstractas tienen un conjunto (deliberadamente) de propiedades pequeñas y restringidas, por lo que debe mecanizar mucho menos antes de poder llegar a los bits buenos.

Las pruebas de teoría de la complejidad y algoritmos / estructuras de datos tienden (como regla) a usar propiedades sofisticadas de dispositivos simples como números, árboles o listas. Por ejemplo, los argumentos combinatorios, probabilísticos y teóricos de números se muestran de manera rutinaria al mismo tiempo en los teoremas de la teoría de la complejidad. ¡Obtener el soporte de la biblioteca del asistente de prueba hasta el punto en que esto es bueno de hacer es bastante trabajo!

Un contexto en el que las personas están dispuestas a trabajar es en algoritmos criptográficos. Existen restricciones algorítmicas muy sutiles por razones matemáticas complejas, y debido a que el código criptográfico se ejecuta en un entorno de confrontación, incluso el más mínimo error puede ser desastroso. Entonces, por ejemplo, el proyecto Certicrypt ha construido una gran infraestructura de verificación con el propósito de construir pruebas verificadas por máquina de la exactitud de los algoritmos criptográficos.

Un ejemplo muy destacado es, por supuesto, la formalización de Gonthiers Coq del teorema de 4 colores en Coq, que utiliza una gran cantidad de combinatoria.

Mi colega Uli Schöpp utilizó la biblioteca ssreflect desarrollada por Gonthier para este propósito con el fin de verificar (y extender ligeramente) también en Coq un resultado de Cook y Rackoff en autómatas gráficos. https://scholar.google.at/scholar?oi=bibs&cluster=4944920843669159892&btnI=1&hl=de (Schöpp, U. (2008). Un límite inferior formalizado sobre accesibilidad gráfica no dirigida. En lógica para programación, inteligencia artificial y razonamiento ( pp. 621-635). Springer Berlin / Heidelberg.)