Por los teoremas, me refiero a los que usted puede encontrar en un curso de licenciatura de matemáticas, no los que usted puede encontrar en un libro de texto de automatizado de pruebas.
Que quiero decir con "demostrado por un equipo" que existe un teorema fue de forma totalmente automática demostrado por un equipo(Automatizado de teoremas).
Yo excluir las verificaciones de los actuales teoremas por medio de una computadora.
Esta es una pregunta relacionada.
De acuerdo a esto, Robando el problema relativo a si un Robbin del Álgebra es un álgebra de boole es un ejemplo importante. Esto fue demostrado en 1996 por el sistema Automatizado de teoremas del sistema EPQ. El enlace contiene más información.
No hay proyecto de Mizar que tiene el objetivo de desarrollar una base de datos de formalmente verificada teoremas matemáticos. El Mizar Biblioteca Matemática contiene una gran cantidad de "estándar" teoremas matemáticos (vea el enlace para ver ejemplos). Sin embargo, los teoremas no son realmente demostró de forma automática, las pruebas son escritas por un ser humano en el Mizar el idioma y luego son verificados (que al final no importa mucho, la cosa más importante es que tenemos una prueba formal que puede ser verificado y manipulados por un ordenador).
Creo que la mayoría de los citados ejemplo es desde hace varios años: pons asinorum. Al menos eso fue un verdadero ejemplo en el que los programadores se sorprendieron de la prueba interesante que no había conocido a sí mismos y que era más probable elegante de Euclides original-pero resultó, que ya era conocido para Vilano.
Uno bien conocido teorema que ha sido formalmente probado es el de la curva de Jordan teorema.
I-Ciencias es una comunidad de estudiantes y amantes de la ciencia en la que puedes resolver tus problemas y dudas.
Puedes consultar las preguntas de otros usuarios, hacer tus propias preguntas o resolver las de los demás.
