La incorporación de modelos de lenguaje de gran escala (LLM) en actividades matemáticas plantea nuevas oportunidades, pero también interrogantes relevantes sobre confiabilidad, autoría y rigor académico. Este trabajo analiza las implicaciones de la inteligencia artificial aplicada al razonamiento matemático a partir de un enfoque neuro-simbólico que combina las capacidades generativas de los LLM con sistemas de verificación formal, particularmente Lean 4. El estudio base emplea un enfoque computacional mixto y considera conjuntos de datos como mathlib y MiniF2F, junto con arquitecturas de generación aumentada por recuperación (RAG) y estrategias de búsqueda de demostraciones mediante Hyper-tree Proof Search.
Los resultados muestran que los sistemas analizados alcanzan una precisión promedio de autoformalización del 74,6 %, con una reducción estimada del 78,5 % del esfuerzo manual requerido para traducir expresiones matemáticas a lenguajes formalmente verificables. Sin embargo, se identifica también un 15,3 % de alucinaciones lógicas en las demostraciones generadas, las cuales son rechazadas por el sistema de verificación formal cuando no satisfacen las reglas lógicas establecidas.
A partir de estos hallazgos, se discuten sus implicaciones para la integridad académica en la enseñanza y producción de conocimiento matemático. Se propone avanzar desde enfoques centrados únicamente en detectar o prohibir el uso de inteligencia artificial hacia modelos basados en transparencia, trazabilidad, verificación y responsabilidad humana. La confianza académica en sistemas generativos no debería sustentarse exclusivamente en la plausibilidad de sus respuestas, sino en la posibilidad de verificar los razonamientos producidos y mantener al usuario como responsable final de su interpretación y validación.
