Can cognitive architectures (CLARION, SOAR, ACT-R, others) be used for creative mathematical reasoning? As far as I understand, then it is the best to encode formal mathematical knowledge in the languages of proof assistants like Coq (CIC - Calculus of Inductive Constructions), Lean, Isabelle/HOL, Mizar. But those proof assistants require manual/creative human invovlement for the tasks like:
- concept/new definition creation, creation of theories;
- formulation of theorems and lemmas (to be proved by proof assistant);
- selection of arguments, selection of proof tactics, invention of new proof tactics;
- goal definition and direction definition in forward reasoning/chaining, e.g. in creating more or less expanded full consequence set from selected set of theorems.
All these tasks require creativity, human-level determination and goal evaluation/selection. So - can these listed activies be done by the cognitive architectures or other computational creativity tools? Is such integration of hard/soft formal/creative proof-assistant/cognitive-architecture tools and approaches under research and development? Is there scientific literature about such integration specifically and about application of cognitive architectures to doing math generally?
Such integration and application can be of immense benefit to humanity. E.g. for the automatic generation and analysis of the algorithms for the optimization, robotics, scheduling etc. For the automatic search of new logics and for the automatic self-improvement of proof assistants and cognitive architectures themselves.