Two thoughts:

1) As far as I recall this program of formalizing mathematics fails unless you banish autoregression.

2) It is important to point out that a theorem in this context is not the same as a "Theorem" from mathematics. Production rules generate theorems that comply with rules and axioms of the formal system, ensuring that they could have meaning in that formal system. The meaning cannot justify the rules though, fortunately, most know to use the rules of logic so that we are not grunting beasts, incapable of conveying information.

I think the author wonders why theorems that don't seem to have meanings appear in the output of AI.