Las personas reales se desenvuelven en situaciones complejas, como la investigación matemática, utilizando el pensamiento metafórico o visual y una intuición perfeccionada desarrollada a través de la experiencia. Gran parte de ello es un razonamiento inconsciente para el que formamos racionalizaciones ad hoc cuando se nos pide; parte de la formación matemática consiste en ser capaz de pulir esas cosas mentales para convertirlas en argumentos abstractos y lógicos. Parte de lo que hace que las pruebas sean bellas, cuando lo son, es que "llegan al corazón de las cosas" e ilustran por qué las cosas son como son. (Las pruebas no siempre son conceptuales e ilustrativas: también pueden ser áridas, tediosas y poco esclarecedoras, y a veces pueden ser, en cambio, elegantes, porque eluden ingeniosamente cualquier requisito para ver lo que sucede).
Los ordenadores no tienen el mismo tipo de proceso creativo. Sin embargo, seguramente podremos hacer que se guíen por algún tipo de proceso no arbitrario que haga que su búsqueda sea más fructífera que la búsqueda bruta aleatoria a través de espacios de cadenas de símbolos (que presumiblemente sería ineficiente hasta el punto de ser un esfuerzo inútil). Además, el tipo de búsqueda creativa de un ordenador podría ser capaz de encontrar cosas que los humanos no fueron capaces de encontrar antes.
Creo que es poco probable que los ordenadores sean capaces de resolver de forma creativa los problemas que los matemáticos consideran más importantes, como los problemas del milenio o el último teorema de Fermat o la clasificación de los grupos simples finitos, aunque puedan ayudarnos en cálculos de memoria como el teorema de los cuatro colores. Sin embargo, esto no es más que una especulación futurista sobre lo cerca que podemos (y conseguiremos) que los ordenadores simulen el pensamiento humano o similar (cualitativamente), y no creo que haya ningún hecho definitivo al respecto.
Sin embargo, los cálculos informáticos pueden hacer algo más que comprobaciones de memoria (prueba por agotamiento). Pueden hacer una validación simbólica, por ejemplo, en las soluciones al problema cuántico de los tres cuerpos de la molécula-ion de hidrógeno, o encontrar patrones numéricos serendípicos que luego pueden conducir, mediante el esfuerzo humano, a nuevos resultados, como la fórmula BPP para los dígitos de $\pi$ o el atractor de Lorenz o la constante de Feigenbaum. Véase el artículo de Wikipedia sobre matemáticas experimentales para más información.
La última cuestión parece entrar en el ámbito de la psicología cognitiva de las matemáticas. Creo que la mayor parte del trabajo en este ámbito se ha realizado sobre el pensamiento más innato presente en los niños y se ha orientado al análisis de los resultados y las estrategias educativas. Sin embargo, algunos seguramente se dirigen a las matemáticas superiores y a qué estructuras cerebrales son responsables de lo que hacen los matemáticos y cómo se pueden modelar los procesos mentales pertinentes.
