FWIW when I first studied automatic theorem proving as a (high school) student in 2013, this was already widely discussed. They were trying to add neural networks inside the solvers, rather than current paradigm of a neural networks using theorem provers as tools. Presumably the history of logic + natural language computers would go back a lot further.