🔢 matemáticas

Proof Assistants at the interplay of mathematical cultures: a semiotic-cultural analysis of proof in higher education

Este artículo emplea un marco semiótico-cultural para analizar cómo los Asistentes de Demostración, específicamente Verbose Lean, funcionan como reveladores epistémicos en la matemática de pregrado al reconfigurar las prácticas de demostración y hacer explícitas las suposiciones implícitas mediante la formalización necesaria de los objetos matemáticos y los pasos inferenciales.

Autores originales: Carola Manolino, Cécile Ouvrier-Buffet

Publicado 2026-10-21

📖 7 min de lectura🧠 Análisis profundo

CC BY 4.0

Autores originales: Carola Manolino, Cécile Ouvrier-Buffet

Artículo original bajo licencia CC BY 4.0 (https://creativecommons.org/licenses/by/4.0/). ✨ Esta es una explicación generada por IA del artículo a continuación. No ha sido escrita ni avalada por los autores. Para mayor precisión técnica, consulte el artículo original. Leer descargo de responsabilidad completo

En el mundo de las matemáticas universitarias, el acto de demostrar un enunciado es más que simplemente resolver un problema; es una práctica cultural. Es una forma específica de pensar, escribir y validar ideas que los estudiantes deben aprender a medida que transitan de la educación secundaria a la educación superior. Durante décadas, los educadores han observado cómo los estudiantes luchan por cerrar la brecha entre los argumentos intuitivos e informales que aprendieron anteriormente y los estándares rígidos y explícitos requeridos en el nivel universitario. Recientemente, una nueva herramienta ha entrado en este panorama: el asistente de demostración. Estos son programas informáticos diseñados para verificar argumentos matemáticos con absoluta precisión, obligando al autor a no dejar ningún paso sin explicar. Mientras algunos ven estas herramientas como una forma de hacer la matemática más rigurosa, otros temen que puedan sofocar la creatividad o confundir a los estudiantes que ya están teniendo dificultades. La cuestión no es simplemente si estos programas ayudan o estorban, sino cómo cambian la naturaleza misma de cómo se escribe y se entiende una demostración.

Un equipo de investigadores de dos universidades francesas decidió observar de cerca esta interacción. No se limitaron a preguntar si los estudiantes aprendían mejor; observaron cómo el programa informático remodelaba el proceso de pensamiento de los estudiantes. El estudio se centró en un curso de primer año donde los estudiantes utilizaban un tipo específico de asistente de demostración llamado Verbose Lean. A diferencia de los lenguajes de programación estándar que parecen código, Verbose Lean permite a los estudiantes escribir en una forma controlada de lenguaje natural, lo que lo hace sentir más cercano a la forma en que los matemáticos hablan y escriben en papel. Los investigadores observaron a una pareja de estudiantes trabajando en un problema clásico: demostrar que si una sucesión de números se acerca cada vez más a un valor positivo, los números en esa sucesión deben volverse positivos eventualmente. Al registrar las conversaciones de los estudiantes, sus garabatos en el papel, su escritura en la pantalla y la retroalimentación de la computadora, los investigadores crearon un mapa detallado de cómo una idea matemática viaja desde un pensamiento vago hasta un hecho verificado por la computadora.

Lo que los investigadores descubrieron fue que la computadora no solo verificaba la respuesta final; actuaba como un espejo, revelando supuestos ocultos que los estudiantes suelen dar por sentados. En una clase de matemáticas normal, un estudiante podría saltarse pequeños detalles o confiar en una "sensación" de que un paso es obvio. La computadora, sin embargo, exige que cada objeto, cada condición y cada salto lógico sea nombrado y justificado explícitamente. El estudio mostró que este requisito fuerza un tipo de cambio cultural. Los estudiantes tenían que traducir sus ideas fluidas e intuitivas en una estructura rígida que la máquina pudiera entender. Este proceso no fue fluido. Implicó un constante vaivén entre las notas de los estudiantes en el papel, sus palabras habladas, los mensajes de error de la computadora y las explicaciones del profesor.

Los investigadores rastrearon una expresión matemática específica que apareció a lo largo del trabajo de los estudiantes. Al principio, los estudiantes trataron esta expresión como un número útil para usar en su razonamiento. Sin embargo, cuando intentaron escribirla en la computadora, el programa la rechazó. La computadora no dijo que el número fuera incorrecto matemáticamente; dijo que el número estaba en el lugar equivocado. Los estudiantes habían intentado usarlo como una etiqueta para una posición en una sucesión, pero la computadora necesitaba un número entero para ese rol, mientras que su expresión era una fracción. Este momento fue un punto de inflexión. Obligó a los estudiantes a darse cuenta de que, en el mundo del asistente de demostración, el rol que juega un número es tan importante como el número mismo. Tuvieron que repensar su estrategia, moviendo la expresión de una parte de su argumento a otra, donde finalmente encajara en las estrictas reglas de la computadora.

Esta lucha no fue resuelta únicamente por la computadora. El profesor, trabajando en la pizarra en la misma aula, dibujó un diagrama para explicar el concepto visualmente. Describió una "ventana" de tamaño que ayudaba a los estudiantes a ver por qué su número debía ser menor que el valor objetivo. Esta explicación visual, combinada con el rechazo de la computadora a su primer intento, ayudó a los estudiantes a reorganizar sus pensamientos. Finalmente comprendieron que el número con el que habían estado luchando no era la posición en la sucesión, sino el tamaño del espacio que necesitaban medir. Una vez que realizaron este cambio, la computadora aceptó su argumento. La demostración final no fue una línea recta desde la idea hacia la solución; fue un viaje complejo donde el significado de un solo símbolo cambiaba dependiendo de si se estaba hablando, escribiendo en papel, explicando mediante un profesor o verificado por una máquina.

El estudio sugiere que los asistentes de demostración actúan como "reveladores epistémicos", un término que los autores utilizan para describir herramientas que hacen visible lo invisible. Revelan los "no pensados" de la matemática —las partes de una demostración que los expertos y estudiantes suelen dejar sin decir porque parecen obvias. En un aula tradicional, estos vacíos podrían pasar desapercibidos. En un aula con un asistente de demostración, la computadora obliga al estudiante a llenar cada vacío, exponiendo las reglas ocultas que gobiernan la validez matemática. Los investigadores argumentan que esto no significa que la computadora sea mejor que el humano, o que el humano sea mejor que la computadora. En cambio, ambos sistemas trabajan juntos para crear un nuevo espacio donde diferentes formas de pensar sobre la demostración colisionan y se fusionan.

Los hallazgos indican que la introducción de estas herramientas cambia la cultura de la demostración en la educación superior. No se trata solo de añadir una capa de rigor técnico; se trata de reconfigurar cómo los estudiantes entienden lo que significa tener razón. El estudio muestra que los estudiantes no simplemente aprenden a escribir código; aprenden a navegar entre diferentes mundos de significado. Deben aprender a traducir su comprensión intuitiva a un lenguaje que una máquina pueda verificar, mientras también escuchan la explicación humana del profesor. Los mensajes de error de la computadora no son solo obstáculos; son señales que le dicen al estudiante dónde su comprensión es incompleta. Al obligar a los estudiantes a hacer explícitos sus supuestos implícitos, estas herramientas proporcionan una oportunidad única para estudiar cómo se construye y se valida el conocimiento matemático.

Finalmente, el artículo concluye que los asistentes de demostración no son herramientas neutrales. Llevan consigo ideas específicas sobre lo que cuenta como un argumento válido. Cuando los estudiantes los usan, no solo están aprendiendo matemáticas; están aprendiendo un nuevo conjunto de reglas culturales sobre cómo pensar y comunicarse. Los investigadores sugieren que este cambio ofrece un lugar privilegiado para estudiar la continuidad y las rupturas entre la forma en que se enseña la demostración, la forma en que la practican los expertos y la forma en que la verifica una máquina. El viaje de los estudiantes en este estudio, desde su confusión inicial hasta su éxito final, ilustra que aprender a demostrar con una computadora es un proceso de traducción. Es un proceso donde el significado de una idea matemática es probado, remodelado y, finalmente, estabilizado a través de la interacción de la intuición humana, la guía del profesor y la precisión de la máquina.

Resumen Técnico: Los Asistentes de Demostración en la Intersección de las Culturas Matemáticas

Planteamiento del Problema
El artículo aborda los desafíos epistemológicos y didácticos que surgen de la introducción de los Asistentes de Demostración (PAs, por sus siglas en inglés) en la educación matemática de pregrado. Mientras que la literatura existente suele evaluar los PAs basándose en si facilitan o dificultan el aprendizaje, este estudio postula que los PAs funcionan como "artefactos culturales" que integran compromisos epistemológicos específicos respecto a la validez, la formalización y la explicitud. El problema central es comprender cómo el uso de los PAs reconfigura las "práctías culturales de la demostración" en la educación superior. Específicamente, los autores investigan cómo la transición de la demostración matemática "ordinaria" (a menudo tolerante con los pasos implícitos) a la demostración verificada por máquina (que requiere una total explicitud) crea fricción, revela supuestos ocultos ("no pensados") y requiere una traducción a través de diferentes sistemas semióticos. El estudio cuestiona cómo estos artefactos digitales hacen visibles las normas implícitas de la demostración que usualmente pasan desapercibidas en los entornos tradicionales de papel y lápiz.

Metodología
La investigación emplea un análisis cualitativo, semiótico-cultural, fundamentado en un marco teórico que combina la Transposición Cultural (Mellone et al., 2019) y la Semiosfera de Lotman (1990).

Contexto: El estudio se sitúa en un curso de primer año de universidad ("Lógica y Demostraciones Asistidas por Computadora") dentro de un programa de doble titulación en matemáticas y ciencias de la computación en Francia.
Herramienta: Los estudiantes utilizaron Verbose Lean, una interfaz de lenguaje natural controlado para el asistente de demostración Lean, diseñada para cerrar la brecha entre el discurso matemático ordinario y la sintaxis formal.
Fuente de Datos: El análisis se centra en un episodio didáctico único que involucra a dos estudiantes (S. y M.) trabajando en una demostración de que "si una sucesión real tiende a un límite estrictamente positivo, entonces sus términos son eventualmente positivos". Los datos incluyen grabaciones de video/audio de las interacciones de los estudiantes, inscripciones en papel, código de Verbose, mensajes de error y una corrección pública paralela por parte del profesor en la pizarra.
Unidad de Análisis: Los autores definen una "Unidad de Análisis" (UA) como un episodio de transposición semiótico-cultural donde un "texto" matemático debe transformarse para moverse entre diferentes sistemas de validación (por ejemplo, de la exploración en papel al feedback del PA). El episodio se segmentó en siete UAs.
Constructo Clave: El análisis se centra en el concepto de "signo-puente" —un objeto matemático (específicamente la expresión $l/2$ ) que circula a través de las fronteras semióticas, cambiando su rol, estatus y condiciones de legitimidad a medida que se desplaza entre el razonamiento del estudiante, el discurso del profesor y la validación computacional.

Contribuciones Clave y Marco Teórico
El artículo contribuye con una lente teórica novedosa para analizar la demostración en entornos tecnológicos:

Los PAs como Reveladores Epistémicos: Los autores argumentan que los PAs no solo añaden rigor, sino que actúan como "reveladores epistémicos" que hacen observables los "no pensados" de la demostración. Estos "no pensados" son supuestos o pasos operativos (por ejemplo, el rol específico de una definición, la gestión de cuantificadores) que funcionan de manera implícita en la demostración ordinaria, pero que deben tematizarse para una máquina.
Transposición Cultural y Semiosfera: Al articular la Transposición Cultural con la Semiosfera, el estudio trata el aula como un espacio semiótico heterogéneo donde coexisten e interactúan múltiples culturas de la demostración (prácticas de la escuela secundaria, prácticas de investigación universitaria, didáctica institucional y verificación computacional).
El Signo-Puente: El artículo operacionaliza el "signo-puente" para rastrear cómo se transforma el significado matemático a través de las fronidades. Demuestra que la relevancia matemática de un signo no garantiza su validez formal; el signo debe ser re-funcionalizado para ocupar el rol estructural correcto dentro de la lógica del PA.

Resultados
El análisis de las siete Unidades de Análisis (UA) respecto a la expresión $l/2$ revela las siguientes dinámicas:

Exploración Inicial (UA1-2): Los estudiantes tratan inicialmente $l/2$ como una cantidad matemáticamente prometedora en el papel. Cuando intentan usarlo en Verbose como un testigo para un número natural ( $N$ ), el PA lo rechaza debido a un error de tipo (número real vs. número natural). Esto resalta la distinción entre utilidad matemática y rol formal.
La Definición como Operador (UA3): Los estudiantes luchan por pasar de tratar la definición de convergencia como un texto estático para ser copiado, a tratarla como un operador que debe ser especializado con parámetros específicos para generar nuevos elementos de contexto.
Mediación Institucional (UA4): La corrección pública del profesor introduce una metáfora de "ventana" (visualizando el límite en una recta real) y coordina explícitamente la elección de $l/2$ con la definición de convergencia. Este discurso actúa como un recurso semiótico institucional disponible en la semiosfera del aula.
Re-funcionalización (UA5-6): Los estudiantes construyen inicialmente una estructura de demostración usando $l$ como parámetro, la cual falla al no lograr la positividad estricta. Eventualmente, re-funcionalizan $l/2$ , moviéndolo del rol rechazado de testigo ( $N$ ) al rol correcto de un parámetro real positivo ( $\epsilon$ ) utilizado para especializar la hipótesis de convergencia.
Redistribución de la Validación (UA7): La demostración final es aceptada solo después de que la cadena algebraica es justificada localmente paso a paso para el PA. Se demuestra que la validación está distribuida: depende de la exploración del estudiante, el discurso institucional del profesor, las definiciones matemáticas y, finalmente, la verificación computacional.

Significado y Pretensiones
El artículo sostiene que la introducción de los PAs reconfigura fundamentalmente la epistemología de la demostración en la educación superior al:

Revelar Prácticas Implícitas: Los PAs obligan a los estudiantes a hacer explícitos objetos, tipos, cuantificadores y pasos inferenciales que suelen ser implícitos en las demostraciones "ordinarias", exponiendo así los "no pensados" de la práctica matemática.
Redistribuir la Validación: El estudio demuestra que la validez en un entorno mediado por un PA no es un estado binario alcanzado al final, sino un proceso distribuido que involucra múltiples autoridades (estudiantes, profesores, normas institucionales y la máquina).
Destacar la Fricción de la Traducción: La investigación muestra que la transición entre culturas de demostración no es una progresión lineal, sino un proceso complejo de traducción donde los signos deben cambiar de estatus. El concepto de "signo-puente" permite a los investigadores observar dónde estas traducciones tienen éxito o fallan.
Conclusión Modesta: Los autores no pretenden que los PAs mejoren automáticamente el aprendizaje o que los estudiantes integren sin problemas el discurso del profesor con los requisitos formales. En cambio, destacan que, si bien los PAs hacen visibles las prácticas culturales, la "falta de alineación" entre el discurso del profesor y la actividad del estudiante dentro del PA sigue siendo un desafío estructural. El estudio hace un llamado a cambiar el enfoque de la investigación de la evaluación de la eficiencia de los PAs hacia la comprensión de cómo estas herramientas reconfiguran fundamentalmente la enseñabilidad y la epistemología de la demostración matemática.

Más como este