4 ms·
How about using http://us.metamath.org/ http://us.metamath.org/ as a db for math theorems / definitions and do some heavy data mining there?
by samuel2 6y ago
How about using http://us.metamath.org/ http://us.metamath.org/ as a db for math theorems / definitions and do some heavy data mining there?
- raphlinus 6y agoThere's some work on this already, including Holophrasm and work by OpenAI on proof shortening. These efforts are linked from the Metamath wiki: https://github.com/metamath/set.mm/wiki/Automated-proving https://github.com/metamath/set.mm/wiki/Automated-proving
- samuel2 6y agovery cool, thanks for sharing
- dwheeler 6y agoOpenAI 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 https://m.youtube.com/watch?v=LVGSeDjWzUo Note that near the end, one of the contributors is OpenAI, who is not a human contributor.