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