empirical metamathematics

[José Manuel Rodríguez Caballero]

Dear FOM members,
  Recently, S. Wolfram [1] published his independent research on an
empirical approach to metamathematics. In this approach, the fundamental
concept is the theorem network, which is a directed graph, which has the
theorems as vertices and there is an arrow from the theorem x to the
theorem y if and only if the theorem x is used in the proof of the theorem
Y. Unlike conventional metamathematics, which is primarily a rationalistic
subject, S. Wolfram proposed an empirical study of the network of theorems
to extract properties of mathematics from data. This approach is similar to
finding the laws of nature from experiments in physics.

  As an example of his method, S. Wolfram did a careful statistical
analysis of the Euclidean Element theorem networks and the Metamath and
Lean proof assistants theorem networks, showing different statistical
distributions in some cases and similar statistical distributions in other
cases.

  In the conclusions of his work, S. Wolfram wrote:

I don’t think empirical metamathematics has been much of a thing in the
> past. In fact, looking on the web as I write this, I’m surprised to see
> that essentially all references to the actual term “empirical
> metamathematics” seem to point directly or indirectly to that one note of
> mine on the subject in A New Kind of Science.


  Motivated by this statement, I would like to ask the following questions:

1) Are there references to empirical work in metamathematics?

2) Is there a theoretical way to explain the statistical distributions
obtained by S. Wolfram in the networks of theorems?

Kind regards,
José M.

References:
[1] The Empirical Metamathematics of Euclid and Beyond
URL =
https://writings.stephenwolfram.com/2020/09/the-empirical-metamathematics-of-euclid-and-beyond/
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20200928/60f5d448/attachment.html>