On the unification problem for polymodal provability logic

The unification problem for a given modal logic is closely related to the problem of characterization of its admissible rules. It is well-known that GL has the finitary unification type (S. Ghilardi), the problem of admissibility of rules is decidable (V.V. Rybakov), and its admissible rules admit a natural axiomatization (E. Jerabek). For the polymodal provability logic GLP, even for the language with just two modalities, these questions mostly remain open.
We show that the fragment J of GLP (in the laguage with finitely many modalities) has a finitary unification type, that is, the set of unifiers of any formula is generated by finitely many maximal ones. At the same time, the unification type of GLP itself (in the language with just two modalities) is nullary, that is, there is a unifiable formula whose set of unifiers does not have a maximal one.
Joint work with L. Beklemishev.