It may be useful to publish a formalization of ALL known mathematics at this point. Like every book ever printed, every paper on arXiv etc.

How many Gigabytes would that be, compressed? Wikipedia once fit on a DVD

This might also allow for some interesting meta-mathematics