A family of infinite subsets of natural numbers is almost disjoint if for any two distinct members of the family, their intersection is finite. The classical theorem of Mathias from the 70s states that there is no infinite analytic maximal almost disjoint (mad) family. The original proof used forcing and it wasn't until almost four decades later that Asger Törnquist found a proof which used a derivative process on a tree.
In joint work with Asger Törnquist, we managed to simplify the derivative process so that it can be carried out (and it terminates) in LωCK1Lω1CK, thus proving that for any infinite Σ11Σ11 almost disjoint family, there is a Δ11Δ11 witness to non-maximality (where both classes are lightface). The ongoing work in progress attempts to generalise the result to the ideals FinαFinα for α<ωCK1α<ω1CK.
This is joint work with Asger Törnquist.