The first challenge will be the selection of a suitable proof assistant. Initial research by Stefan Rass resulted in the two preliminary candidates Isabelle/HOL and Coq. They seem similar in many respects, both having a refined set of features and both having been in development for more than 30 years, with an active community and steady support.

As outlined in the Comparison, Coq is easier to use for small-scale precise manipulation (for example, rewriting the current proof goals) and Isabelle provides powerful automatic solvers that help prevent small-scale manipulations from being necessary.

• Proof Assistants
  • Isabelle Overview
    • Useful Settings
    • Simpl (imperative program verification framework for Isabelle)
  • Coq Overview
  • Comparison of Isabelle and Coq
• P vs NP
  • Claimed Solutions of P vs NP
  • Meta Results on Proofs Surrounding P vs NP
• Sources, Resources, Literature and Further Reading