Right now, I think I would go for that classical approach, simply because there is more supporting material for that in the library, and there are more people who understand that approach and can help contributing. (I'm talking specifically about functional analysis and PDEs here.)

On the other hand, it should be a lot of fun to see if we can formalize the new proof by Clausen--Scholze of Serre duality. Using their machinery, the proof should simplify a lot. But this requires building complex analytic manifolds on top of condensed mathematics. So we would first need to set up those foundations.