my question is : is it possible to define in some way what should do an "optimal automatic mathematician" ?

There are two points of view of an automatic theorem prover / automatic mathematician :

(1) you define a theorem you wish to prove, the prover, if the theorem is provable, answers a proof of the theorem.

(2) you define a context (a language with its syntax and symbols, some axioms, a set of rules of deduction), then the automatic mathematician will explore all the mathematics world engendered by this context, and will enumerate some theorems (with their proofs).

Even if I can't prove it formally, it is easy to see that if many important theorems are unknown to the prover, and if in (1) you ask it to prove a very very difficult theorem, the prover will have to prove at first many others theorems, in order to prove the one you asked. Thus, (2) is equivalent to (1): an automatic mathematician is equivalent to an automatic theorem prover. In any case, the prover has to do the job of a mathematician : explore the world of mathematics, finding new proofs of new theorems.

I think there are at least 4 important criterion when comparing automatic mathematicians :

  • time consumption,

  • memory consumption,

  • readability/sparsity : proofs and theorems statements should be understandable by a human. This means that the concepts and mathematical objects involved in proofs should be organized in a smart/relevant way. this means for example it cannot avoid some sort of set theory (so that the language used by the program is close to the way we express maths every day : the concept of set is a very important mathematical concept). the automatic mathematician should also store in memory some theorems and their proofs (often, there are more interesting math concepts in the proof of a theorem, than in the theorem itself), with also some new symbols stored (new functions, new sets, new operators...) so that the concepts involved in theorems and proofs are easy to understand. obviously, only a small number of theorems and symbols should be stored : the automatic mathematician has to decide (and it's probably the hardest part) whenever a mathematical object is an interesting concept in itself or not,

  • completeness : the automatic mathematician should explore/enumerate (nearly) every interesting mathematical concept, and be able to proof (nearly) every provable theorem, for example we don't want of an automatic mathematician avoiding Pythagore's theorem and trigonometric functions...

After all that, I think the Pythagore theorem and the construction of trigonometric functions is exactly what we have to inspect in details in order to define how should be an automatic mathematician. The way the concept of 2-dimensional geometric space calls for : norm, triangles, surfaces, Pythagore theorem, which leads to the unit circle and trigonometric functions. These are very simple mathematical concepts when you know them, but creating those while they haven't been defined yet is exactly what we expect from a genious mathematician.

  • $\begingroup$ I don't think that (2) is equivalent to (1). A theorem prover might have a thousand or even a million sub-results along the way to prove a certain theorem, but not know which are interesting and which are boring. $\endgroup$ – Charles Jun 29 '15 at 16:04
  • $\begingroup$ Most theorem provers are of type (1), and usually they are quite limited -- in a practical sense you ask them to prove small steps toward a theorem, but you still have to map out the path. The only example I know of for (2) is Colton's HR. $\endgroup$ – Charles Jun 29 '15 at 16:05
  • $\begingroup$ @Charles : yes but if it just explores randomly the space of proofs to find one corresponding to the theorem, it will take some huge time... it doesn't work for larges theorems : the only way to proof (in a reasonable time) some hard theorems is to understand concepts. and in some way, the stupid random exploring automatic prover is equivalent to the automatic mathematician storing every theorem, storing $f(a) > 0$ but also $f(a) + 1 > 1$ and $f(a) + 14 > 14$... $\endgroup$ – reuns Jun 29 '15 at 16:09
  • $\begingroup$ But we don't have any automated provers which understand concepts in that sense. They're much smarter than the random prover but not at all insightful. $\endgroup$ – Charles Jun 29 '15 at 16:15
  • $\begingroup$ no all provers from the wikipedia's list are of this type : they start from the theorem and try to reduce it to tautology, randomly exploring a tree. this is why I finish with the "2d geometry $\implies$ Pythagore $\implies $ trigonometry" problem. I think it is a very good example of the "concept understanding problem". $\endgroup$ – reuns Jun 29 '15 at 16:18

I believe a rigorous account of mathematical beauty is key to building an optimal theorem proving agent. Some work in that direction has been done by Jürgen Schmidhuber (http://people.idsia.ch/~juergen/) who has linked beauty in general to the concept of compression.Taking algorithmic information theory as the basis we can then define "interesting" (or "beautiful" or "powerful" ) results as those with broad applicability - which enable the agent to come up with a compressed representation of the space of possible proofs. The idea being that a collection of powerful theorems reduce the branching rate of a "random" search through proof-space to something very close to 1, though not quite 1 as that would imply knowing the proof already. Without drastically lowering the branching rate of search procedures, you accomplish nothing whatsoever - an order of magnitude increase in total computing power available to find a proof of length $n$ allows the branching rate to increase by something like a tenth, or perhaps a hundredth (I can't recall precisely from when I calculated this, but it's not a hard calculation to do yourself).

Some theoretical considerations owed to Gödel's incompleteness theorems, Tarski's undefinability theorem and the Duhem-Quine thesis on the vulnerability of "analytical" knowledge to modification on the basis of experience lead me to believe that you'd need to base your system on principles of non-axiomatic reasoning. Which is not to say that it should be impossible to reason within axioms, but it should be able to doubt its own axioms and not take them for granted for all time. I believe paraconsistent logic may be of assistance in building an agent capable of this. This will enable the agent to invent broader theories than those strictly implied by any particular axioms, such as non-euclidean geometries (or group theory to attack the problem of quintics).

I've collected these notions by searching for clarification about my own intuitions of how formal reasoning works. Unfortunately I am not a very talented mathematician (actually to be frank, I frequently struggle with what seems easy to others), so I cannot begin to imagine the internal contours of the minds of geniuses. I would be quite pleased to hear more ideas on this neglected research area (I don't consider resolution theorem provers and the like to be serious attempts at building competent mathematical agents).


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.