Uso de asistentes de demostración en la enseñanza de las matemáticas

El proyecto consiste en introducir el uso de asistentes de demostración en el grado en matemáticas. Este primer año, proponemos realizar una prueba piloto en las asignaturas de números y conjuntos (primer curso), y topología general (segundo curso).

La prueba consistirá en desarrollar material que recorra las definiciones, enunciados y demostraciones vistas en el curso, en el asistente de demostración Lean [1]. Idealmente, este material cubriría todo el curso. Algunos de los enunciados estarán demostrados, y en otros las demostraciones se dejarán como ejercicios. Este material se subirá al anillo digital docente para que los alumnos lo puedan consultar, y realizar los ejercicios.

Dependiendo de la disponibilidad de tiempo, implementaremos una herramenta online para corregir las producciones de los alumnos. Este aspecto no es prioritario puesto que el propio software usado por los alumnos les proporciona el feedback necesario.

También en el ADD realizaremos encuestas a los alumnos sobre cuánto han usado Lean, cómo de útil les ha parecido como herramienta, y en qué medida les ha ayudado a desarrollar competencias transversales relacionadas con el pensamiento riguroso y la demostarción formal.

[1] https://leanprover-community.github.io/