'Proving Theorems' is a grand sounding statement, but the reality need not be so glamorous! A Theorem as a thing is an encapsulation of a granule of knowledge o

'Proving Theorems' is a grand sounding statement, but the reality need not be so glamorous! A Theorem as a thing is an encapsulation of a granule of knowledge or, even less precisely, something learnt which is known to be true[1]. To prove a Theorem is to show that the knowledge it encapsulates is correct. Why is this good? Most theory I have read[2] on AI, machine learning, and knowledge deals in depth with the concept of symbols and symbol manipulation. Some would claim (correctly!) that computers are in essence simply symbol manipulation machines. The thing is, these symbols are really just ways of encapsulating a piece of information. Often, symbols are described as being 'made-up' of other symbols; symbols are used to describe other symbols. As a simple and obvious example: - bits (low level 'axiomatic' symbols) are organised into groups to create bytes (still low level, not much meaning here yet) - bytes are associated with letters (in an isomorphic relation which imparts meaning[3]) - letters are organised into groups to form words (a significant amount of meaning has now appeared) - words are strung together in sentences - sentences are woven into paragraphs/chapters/themes/poems/stories/epics If I was to claim that a poem or story has no meaning simply because I can craft it from simple bits I would be missing something very important about symbol manipulation. When I take a collection of ideas, snippets of information and learning, and am able to label them with a name I can transcend my current level of understanding and deal with ideas which are invisible on the lower level. For a programmer, this hierarchy of symbols presents itself as a hierarchy of low, medium and high level languages. Writing a python program in assembly would be absurd!(although perhaps appropriate in some cases) Theorems (and Axioms) are the symbols of mathematics, and proving Theorems is symbolic manipulation in one of its purest forms. In fact, proving Theorems is the main way in which new 'meaningful'[4] symbols are created. So why is proving Theorems useful? In short, because it is how new knowledge is created! (in this context, mathematical knowledge) Is mathematical knowledge useful? I think anyone living in this modern world of ours (and I think that phrase applies to most people in most of humanity's history) can see that at least some mathematics is useful. Many have here argued about the different merits of developing mathematical knowledge (ie proving Theorems) before an application is well known, so I won't labour that point. Instead, I think I'll direct the interested reader to G.H. Hardy's 'A Mathematician's Apology'[5] for a great essay on the many merits a joy of mathematics can bring the suitably inclined soul. If knowledge is a good thing, and proving Theorems increases knowledge, than proving Theorems is a good thing. To say it is better than other ways of spending our efforts is hard, but I think we can definitely agree that it is useful. [1] My own definition! [2] Which is tragically less than I would like [3] Douglas Hofstadter in Gödel, Escher, Bach explains this idea so much better than I can - see https://en.wikipedia.org/wiki/Gödel,_Escher,_Bach https://en.wikipedia.org/wiki/Gödel,_Escher,_Bach [4] An idea again borrowed from Hofstadter. We can string any string of words together that we want, doesn't mean that they mean anything to us. Formal system such as mathematics give us a way to combine symbols to give us new meaningful symbols. My claim that it is the main way they are created is founded on wild speculation and heavily biased historical observation. [5] http://www.math.ualberta.ca/~mss/misc/A%20Mathematicians%20Apology.pdf http://www.math.ualberta.ca/~mss/misc/A%20Mathematicians%20A...