Maehara’s lemma provides a method for extracting interpolants from cut-free proofs, however, extending interpolation to proofs with cuts has remained challenging. In this paper, we present a generalization of Maehara’s lemma to admissible cuts – a class of cut-formulas characterized by structural constraints induced by partitions of the end-sequent. We apply our results to the Ceres cut-elimination method, and show that our method not only generalizes earlier results on atomic cuts but also reduces the asymptotic complexity of interpolant extraction from cubic to quadratic. Furthermore, we extend our framework to Lyndon interpolation, establishing both Craig and Lyndon interpolation for proofs with admissible cuts, thereby broadening the applicability and efficiency of interpolation techniques in proof-theoretic reasoning.
