Proof assistant usage in complexity theory research?

A general rule of thumb is that the more abstract/exotic the mathematics you want to mechanise, the easier it gets. Conversely, the more concrete/familiar the mathematics is, the harder it will be. So (for instance) rare animals like predicative point-free topology are vastly easier to mechanize than ordinary metric topology.

This might initially seem a bit surprising, but this is basically because concrete objects like real numbers participate in a wild variety of algebraic structures, and proofs involving them can make use of any property from any view of them. So to be able to the ordinary reasoning that mathematicians are accustomed to, you have to mechanize all these things. In contrast, highly abstract constructions have a (deliberately) small and restricted set of properties, so you have to mechanize much less before you can get to the good bits.

Proofs in complexity-theory and algorithms/data-structures tend (as a rule) to use sophisticated properties of simple gadgets like numbers, trees, or lists. Eg, combinatorial, probabilistic and number-theoretic arguments routinely show up all at the same time in theorems in complexity theory. Getting proof assistant library support to the point where this is nice to do is quite a lot of work!

One context where people are willing to put in the work is in cryptographic algorithms. There are very subtle algorithmic constraints in place for complex mathematical reasons, and because crypto code runs in an adversarial environment, even the slightest error can be disastrous. So for example, the Certicrypt project has built a lot of verification infrastructure for the purpose of building machine-checked proofs of the correctness of cryptographic algorithms.

Solved by user657 (31,628 )
May 31, 2017 at 15:54