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 https://www.youtube.com/watch?v=Is_lycvOkTA (see below) by Thomas Hales again recently, since he seemed to be striking similar chords in places.