Absolutely not, and for far more reasons than I enumerate below.
The language used to encode the search space will be under constant development and expansion.
The creation of the axioms of any proof system is not a search problem.
Recognition of "meaningful" proofs will be extremely hard to automate. The checking of statements does not create mathematical theory, but it is the collection of related statementswhich do.
The search space is likely to be still much too large for proof systems to exhaustly enumerate all meaningful statements in any person's lifetime.
If mathematical statements could be easily checked, it would make mathematical study quite different. But likely much more interesting and fast paced.
The language used to encode the search space will be under constant development and expansion.
The creation of the axioms of any proof system is not a search problem.
Recognition of "meaningful" proofs will be extremely hard to automate. The checking of statements does not create mathematical theory, but it is the collection of related statementswhich do.
The search space is likely to be still much too large for proof systems to exhaustly enumerate all meaningful statements in any person's lifetime.
If mathematical statements could be easily checked, it would make mathematical study quite different. But likely much more interesting and fast paced.