empirical metamathematics

Timothy Y. Chow tchow at math.princeton.edu
Wed Sep 30 09:39:56 EDT 2020

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 


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.


More information about the FOM mailing list