Utilisation d'un assistant de preuve dans la recherche sur la théorie de la complexité?

Compte tenu des sujets abordés lors d'une conférence comme le STOC, des chercheurs en algorithmes ou en complexité utilisent-ils activement COQ ou Isabelle? Si oui, comment l'utilisent-ils dans leurs recherches? Je suppose que la plupart des gens n'utiliseraient pas de tels outils car les preuves seraient de trop bas niveau. Quelqu'un utilise-t-il ces assistants de preuve d'une manière qui est essentielle à leur recherche, par opposition à un bon supplément?

Je suis intéressé car je pourrais commencer à apprendre l'un de ces outils et ce serait amusant de les découvrir dans le contexte des preuves de réductions, de correction ou de durée d'exécution.

Une règle générale est que plus les mathématiques que vous voulez mécaniser sont abstraites / exotiques, plus elles deviennent faciles. Inversement, plus les mathématiques sont concrètes et familières, plus elles seront difficiles. Ainsi (par exemple) les animaux rares comme la topologie prédictive sans point sont beaucoup plus faciles à mécaniser que la topologie métrique ordinaire.

Cela peut initialement sembler un peu surprenant, mais c'est essentiellement parce que des objets concrets comme des nombres réels participent à une variété sauvage de structures algébriques, et les preuves les impliquant peuvent utiliser n'importe quelle propriété de n'importe quelle vue. Donc pour être capable de raisonner comme les mathématiciens sont habitués, il faut mécaniser toutes ces choses. En revanche, les constructions très abstraites ont un ensemble de propriétés (délibérément) petit et restreint, vous devez donc mécaniser beaucoup moins avant de pouvoir accéder aux bons morceaux.

Les preuves en théorie de la complexité et en algorithmes / structures de données ont tendance (en règle générale) à utiliser des propriétés sophistiquées de gadgets simples comme des nombres, des arbres ou des listes. Par exemple, les arguments combinatoires, probabilistes et théoriques des nombres apparaissent systématiquement tous en même temps dans les théorèmes de la théorie de la complexité. Obtenir le support de la bibliothèque d'assistant de preuve au point où cela est agréable à faire représente beaucoup de travail!

Un contexte dans lequel les gens sont prêts à travailler est celui des algorithmes cryptographiques. Il existe des contraintes algorithmiques très subtiles en place pour des raisons mathématiques complexes, et parce que le code cryptographique s'exécute dans un environnement contradictoire, même la moindre erreur peut être désastreuse. Ainsi, par exemple, le projet Certicrypt a construit de nombreuses infrastructures de vérification dans le but de construire des preuves vérifiées par machine de l'exactitude des algorithmes cryptographiques.

Un exemple très important est bien sûr la formalisation de Gonthiers Coq du théorème des 4 couleurs dans Coq qui utilise beaucoup de combinatoire.

Mon collègue Uli Schöpp a utilisé à cet effet la bibliothèque ssreflect développée par Gonthier afin de vérifier (et d'étendre légèrement) également dans Coq un résultat de Cook et Rackoff sur les automates graphiques. https://scholar.google.at/scholar?oi=bibs&cluster=4944920843669159892&btnI=1&hl=de (Schöpp, U. (2008). Une limite inférieure formalisée sur l'accessibilité des graphiques non orientés. Dans Logic for Programming, Artificial Intelligence, and Reasoning ( pp. 621-635). Springer Berlin / Heidelberg.)