Formally Verified Complexity Theory Is there any ongoing project to formally verify the theorems and proofs of complexity theory using a proof assistant like Coq? Are there any boundaries to doing this?
In the following paper my colleague Uli Schöpp presents a formal verification (in Coq)  of a nontrivial result by Cook and Rackoff on the computational power of graph automata. https://scholar.google.at/scholar?oi=bibs&amp;cluster=4944920843669159892&amp;btnI=1&amp;hl=de (Schöpp, U. (2008). A formalised lower bound on undirected graph reachability. In Logic for Programming, Artificial Intelligence, and Reasoning (pp. 621-635). Springer Berlin/Heidelberg.)