Elementos de matemáticas formalizados en Isabelle/HOL

Abstract

La finalidad de este trabajo es la formalización de teoremas de diferentes teorías de las matemáticas. Para ello, se han elegido una serie de teoremas de la teoría de números, teoría de conjuntos, teoría de funciones, teoría de retículos y teoría de geometría. Una vez formalizados los mismos en el sistema de pruebas automáticas Isabelle/HOL, se han utilizado teorías ya predefinidas en él y comprobado la similitud existente entre la demostración en lenguaje natural y la demostración formal.

The purpose of this project is the formalization of theorems from differents mathematic’s theories. For it, some theorems have been choosen from number theory, set theory, function theory, lattice theory and geometry theory. Once they have been formalized by the automatic proof system Isabelle/HOl, theories have already been used predefined in it and checking the existing similarity between proof in natural language and formal proof.