Hacker News Reader

How about using http://us.metamath.org/ as a db for math theorems / definitions and do some heavy data mining there?

There's some work on this already, including Holophrasm and work by OpenAI on proof shortening. These efforts are linked from the Metamath wiki:

very cool, thanks for sharing

OpenAI has managed to derive a number of Metamath proofs, some of which are smaller than the human-created proofs, using machine learning.

Here is a gource visualization of metamath proofs overtime in the set.mm database: https://m.youtube.com/watch?v=LVGSeDjWzUo

Note that near the end, one of the contributors is OpenAI, who is not a human contributor.