Vladimir_Nesov comments on Today’s xkcd is relevant to our interests

[Vladimir_Nesov]

Be sure to construct some tautologies complicated enough to be useful.

[Pavitra]

Presumably the desired feature is not so much “true” or “true and complicated”, but “useful and non-obviously true”.