Razonamiento formalizado para la enseñanza de las matemáticas

Un posible campo de aplicación del razonamiento formalizado podría ser su uso como alumno inteligente de forma que “enseñar” al sistema sería una manera de aprender a enseñar, haciendo explícito gran parte del conocimiento implícito.

Parece que una idea parecida pudo tener N.G. de Bruijn (el autor de Automath, el primer sistema de razonamiento formalizado) al afirmar que

If you can’t explain your mathematics to a machine it is an illusion to think you can explain it to a student.