Mathematical proofs are one of the pillars of mathematics at a universal level. This fact, added to the difficulty presented by university-level students with mathematical proofs, has led theorists in educational mathematics to propose solutions to these students. In this sense, the use of mathematical proofs assistant software is one of the ways to consider. That is why a computer tool has been developed within the Odoo system. This has the main objective of putting together formal demonstrations based on first-order logic. In this work, some of the general considerations about math proof wizards (particularly the one developed in Odoo) are presented, these being of the type: logical mathematical, computational and educational; Likewise, educational activities are described within this computer program, in order to contribute to the knowledge about the formal proof in students of the first semesters of the Faculty of Mathematics Physics at UMSNH.
Las demostraciones son uno de los pilares de la matemática a nivel universal, este hecho sumado a la dificultad presentada por estudiantes de nivel universitario para con las pruebas matemáticas, ha llevado a teóricos en matemática educativa a proponer soluciones a estos alumnos. En este sentido, el uso de software asistente a demostraciones es uno de los caminos a considerar. Es por ello que se ha desarrollado una herramienta informática dentro del sistema Odoo, esta tiene el objetivo principal de armar demostraciones formales con base en la lógica de primer orden. En este trabajo, se discuten algunas de las consideraciones generales sobre asistentes de pruebas matemáticas (particularmente el desarrollado en Odoo), siendo estas del tipo: lógico matemático, computacional y educativo; así mismo, se describen actividades educativas dentro de este programa, con el fin de contribuir al conocimiento sobre la demostración formal en alumnos de primeros semestres de la facultad de físico matemáticas en la UMSNH.
