Performance problems in theorem provers is an old topic. I remember watching this and it was fun.

https://youtu.be/m-iGCCuHBvY

[Talk] 10 years of superlinear slowness in Coq (2022)