Are there aritficial intelligence methods in mathematics, automatic theorem discovery and proving? Google gives results in the opposite direction - mathematical methods of AI.
Are there applications of neural networks (connection science - neuro-symbolic computation), hypercomputation and cognitive architectures (like SOAR) into the automatic theorem discovery and proving? There is vast literature about symbolic computation (Elsevier has journal about this) but it is limited endeavor due to the Goedel incompleteness theorems. So - methods that more closely model human reasoning can be of help for automatisation of mathematical discoveries.
Just some pointers to the development of the field - there is formalized mathematics branch with the de Gryuter journal "Formalized Mathematics". There is univalent foundation and homotopical type theory as new foundation and formalization of mathematics. Coq and Agda are practical proof assistants in this field. There is also Mizra system.
The question remains - can all this be used for discovery of new theorems and not for just checking of existing theorems. Maybe discovery cycle goes - probabilistic generation of statement in the formal language and subsequent proof or rejection by the prood assistant?