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.
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).