empirical metamathematics

[Timothy Y. Chow]

JMRC wrote:

> Recently, S. Wolfram [1] published his independent research on an 
> empirical approach to metamathematics.

This seems related to work done by Josef Urban and others.  Back in 
November 2013, I posted a question about "Unreasonable effectiveness" to 
FOM.

https://cs.nyu.edu/pipermail/fom/2013-November/thread.html

See in particular the replies by Jacques Carette and Josef Urban.  Here's 
a short list of some references that Josef Urban emailed me back then:

> [1]: http://dx.doi.org/10.1007/s10817-004-6245-1
> [2]: http://dx.doi.org/10.1007/978-3-642-31365-3_30
> [3]: http://www.easychair.org/publications/?page=2069121719
> [4]: http://arxiv.org/abs/1211.7012
> [5]: http://dx.doi.org/10.1007/978-3-642-28717-6_6
> [6]: http://link.springer.com/chapter/10.1007/978-3-642-36675-8_13

In general, the concept of applying machine learning to a corpus of 
formalized mathematics is very old, even if people haven't used Wolfram's 
buzzword "empirical metamathematics" for it.  Of course, today we have 
better software and data than ever before to run such experiments.

Tim