Comment by Ericson2314

The author should try some more modern formal methods.

Tools like Lean and Rocq can do arbitrary math — the limit is your time and budget, not the tool.

These performance questions can be mathematically defined, so it is possible.