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

This is what they are trying to do with Lean

Oh? Where can i read more about that? It appears the sole focus so far was solving open problems

	▲	mattmar96 an hour ago \| parent [-]
		I believe that is the goal of MathLib, to transcribe all math into a big Lean library. https://lean-lang.org/use-cases/mathlib/