I imagine the author was comparing it being subpar at what _they_ do as a contrast to it being excellent at formalizing mathematical theorems. Thus suggesting that there is a significant "spikiness" to AI.