Discoverable Math Requires Structure

Source: Tim Gowers blog, May 2016

<the following is a comment>

To me to be able to fully disseminate mathematics sideways means that it must be formalised, however unfashionable amongst the majority of mathematicians this continues to be. The reason is that with formalised mathematics you have a corpus that is discoverable and usable, although I’m searching for the words here.

I don’t think that formalisation is an end in itself and nor do I think that a formalised proof is necessarily any more worthy just because it has been verified by a computer. It just seems that it’s the only true place to start.

I think that mathematics that has been formalised has a structure and nature that somehow makes it much more amenable to being discoverable, reusable, searchable, etc.

I got very excited when I watched a talk (see below) by Thomas Hales again recently, since he seemed to be striking similar chords in places.

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Google photo

You are commenting using your Google account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s

This site uses Akismet to reduce spam. Learn how your comment data is processed.