In 2002, L.C. Paulson gave a mechanized proof of the consistency of the axiom of choice by formalizing $V=L$ and its consistency. We could ask whether there is a formalized proof of the independence of the continumm hypothesis (abbr. CH).
I have read the article mentioned above, and I know that he does not provide a full metatheory, but only some instantiations required to achieve his goal; for example, he does not prove the fact that every $\Delta_0$-formula is absolute w.r.t. transitive models. Instead, he only proves the absoluteness of some useful concepts.
In the entire article, the author avoids metatheoretic arguments as much as possible. I didn't understand the reason why he did that, though it was very difficult in that time. We cannot hope, however, to formalize forcing arguments because it heavily relies on metatheory. For example, a forcing relation $p\Vdash \phi$ is defined for every formula $\phi$, so the definition of a forcing relation is in fact a metadefinition for each formula $\phi$.
Is the difficulty to handle metatheory the reason why nobody has tried to formalize the forcing arguments and the independence proof of the continuum hypothesis? 15 years have passed from when that article appeared, so I hope someone has found a way to formalize meta-arguments.
In short, my question is:
Is there any attempt to mechanize an independence proof of CH?
If not, what makes it so difficult? I guess handling metamathematics causes a problem. Is that right?