ABSTRACT. The aim of this presentation is to illustrate the use of formal methods in order to reason in the theory of weak mega-categories. The formalism considered here is based on the type theory CaTT introduced by Finster and Mimram, extended with some metatheory on top of it, with an implementation

We first present how the system works and can be used, and then develop some ``real-world'' examples, such as the definition of the braidings in k-tuply monoidal omega-categories (following the terminology of Baez), k>= 2, with the aim of showing that we have a syllepsis in the case k<= 3. These developments have motivated metatheoretical improvements to the proof assistant, which we also present and discuss here, in order to handle and partly automate large proofs.