[openquery]

Proving a theorem given a set of axioms is a search problem. Given a set of axioms you can apply rules of inference to generate the graph of all provable theorems. Proving a theorem is about finding a path from the axioms to the vertex which is your theorem.

But you can make the same case for axioms - that they are not invented but discovered through a process of search in the space of axioms.