empirical metamathematics

[Josef Urban]

There has been quite a bit of work done on analyzing formal math libraries,
importance of lemmas, etc. The Mizar people have been doing this already in
the 90's. A quick more recent self-citation is
https://doi.org/10.1016/j.jsc.2014.09.032 .

Josef

On Tue, Sep 29, 2020 at 5:45 AM José Manuel Rodríguez Caballero <
josephcmac at gmail.com> wrote:

> 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/20200929/b30a6198/attachment-0001.html>