In a sense mathematics already is experimental, because we already have, although not formally defined, class of things where we simply don't know their status

In a sense mathematics already is experimental, because we already have, although not formally defined, class of things where we simply don't know their status of being true or false - hypotheses. I am currently thinking how to make an automated mathematician based on lambda calculus, which would have its own notion of "beauty", and based on this it would try to select interesting definitions. It seems such a system needs to have a notion of experiment. Since computations are proofs, theorems are basically computations that we know the result of already, i.e. which have already been done (all with respect to some axiomatic system, given by types). Such system also needs notion of "economy", which lets it allocate computational resources effectively. So it needs to be able to evaluate things only partially, to avoid infinite loops etc. This naturally leads to experimental approach, where you don't only know true or false, but there is a wide spectrum of what you know about certain statement (lambda expression).