Formalized priority argument A priority argument, an important proof technique in recursion theory, was introduced by Friedberg and Muchnik, to solve Post's Problem, i.e., the existence of two r.e. sets that do not Turing reduce to each other.  

My question is whether or not there has been an attempt to formalize priority arguments in some proof system adopted by proof checkers or proof checkers.  I believe this is an interesting problem, since:


Priority arguments can sometimes be very complicated (for humans to read);
Objects constructed by priority arguments are constructive (relative to something else), so it is possible that the argument is suitable to formalize in some proof systems, many of them are based on typed lambda calculi; and
Yet most construction in priority arguments do not look like a typical functional programs at all
Computability theory in general has been somewhat under-formalized. The short answer is that most theorems of computability theory do not pass one of the three tests for formalization:


A proof that is computationally intensive or untrusted for some reason (long, complex).
A result that is relevant to undergraduate mathematics.
A result that is useful to program verification.


Reason 1 may apply in this case, but the preliminary work to build up to that result unfortunately hasn't been carried out. I found one reference to mechanized computability theory by Xu, Zhang and Urban in Isabelle. It falls significantly short of priority results though.