I am currently reading Why did AM run out steam?, an article regarding Douglas Lenat's Automated Mathematician (AM). AM is an early example (from 1976) of a "discovery system" - a system that attempts to "discover" new concepts from a selection of concepts given to it. In the case of AM, it was designed to have "110 basic concepts of set theory" built in, along with some inference rules.
What I found fascinating about this project was that AM was able to "discover" Goldbach's conjecture! There seems to have been some similar projects to this afterwards, but nothing on a comparable scale to the novelty that AM presented (that I'm aware of).
Crucially, (as the title of the article gives away) AM "ran out of steam" in that it was unable to make any new discoveries after this, it just kept on making the same ones after a while. Many reasons are given for this, including the absence of communication with other systems and theorem proving ability.
This article later states,
"...the development of such a program [which can discover indefinitely] is likely to be some time in the future, since the theorem proving capability would have to be capable of generating new hypotheses in any branch of mathematics it was pursuing, a task beyond current theorem proving methods."
Theorem provers, like Lean,Coq or Metamath are a good sign of development in this area, and the field of AI is growing fast.
Hypothetically, an AI discovery system could be given ZFC (or some similar axiomatic system), some inference rules, and some human feedback of what it means for a theorem to be "meaningful", and just set to run.
My question is given the various technological developments since AM, is there any mathematical (or otherwise) reason why a system like this would "run out of steam", as before? Is generating new hypotheses still beyond current theorem proving methods?