Asistentes de pruebas para las matemáticas

Question

Esta pregunta está relacionada con (tal vez incluso la misma intención que) ¿Introducción a la demostración automática de teoremas / fundamentos lógicos? pero ninguna de las respuestas parece responder a lo que estoy buscando.

Hay muchos recursos disponibles para la gente que quiere utilizar asistentes de prueba como Coq, Isabelle, , para demostrar propiedades sobre los programas, y eso no es una sorpresa, ya que gran parte del desarrollo de estos programas lo hacen los informáticos. Sin embargo, me interesan los recursos, y especialmente en los materiales del curso (porque estoy tratando de armar un estudio independiente para un estudiante de CS), que implica el uso de asistentes de prueba para demostrar matemáticas declaraciones-ver el trabajo de Hales et Weedijk por ejemplo. ¿Alguien conoce alguno?

Answer 1

Sinceramente, parte de la razón por la que los asistentes de pruebas se centran en probar programas es precisamente por nuestra muy limitada comprensión de cómo en realidad representar las matemáticas en sistemas lógicos formales, en lugar de hacerlo en principio.

Resulta que la prueba de programas es básicamente metamatemática aplicada (es decir, la verificación de programas imperativos es teoría de modelos, y la verificación de programas funcionales es teoría de la prueba estructural) y ésta es la única área de las matemáticas en la que la gente realmente ha trabajado con todo detalle cómo representar lo que están haciendo en sistemas lógicos formales. Así que el enfoque en la prueba de programas es, en parte, una virtud de la necesidad. (También es porque a los que estamos en esta área nos gusta mucho tanto la programación como las matemáticas, y esta es una gran manera de combinarlas...)

El número de personas que saben hacer matemáticas de verdad en los asistentes de pruebas y explicarlas a los demás puede contarse con los dedos de la mano. A continuación, un par de sugerencias para añadir a la lista:

• John Harrison escribió un libro reciente, Manual de lógica práctica y razonamiento automatizado que la gente en la que confío habla maravillas. Es una guía de todos los procedimientos de decisión (por ejemplo, la resolución de SAT, la unificación, la aritmética de Presburger, las bases de Groebner, etc.) que necesitas para elevar el nivel de la prueba formal a un nivel decente de abstracción, junto con sus implementaciones en el sistema HOL/Light.

• George Gonthier (que demostró formalmente el Teorema de los Cuatro Colores en Coq) trabaja actualmente en la formalización del Teorema de Feit-Thompson (también conocido como Orden impar) de la teoría de grupos finitos. Como parte de este trabajo, él y sus colaboradores están desarrollando las bibliotecas más sustanciales y la automatización de pruebas para apoyar un estilo de razonamiento más matemático (en lugar de lógico) en Coq. Las guías de este trabajo son "Una formalización modular de la teoría de grupos finitos" y su Biblioteca de componentes matemáticos ( La máquina del retroceso ).

Answer 2

Estoy interesado en el mismo tipo de cosas. Este artículo habla del trabajo realizado para formalizar la teoría de la representación de grupos en Coq. En particular, formalizan la demostración del teorema de Maschke (que $F[G]$ es semisimple cuando $G$ es un grupo finito).

Algunos enlaces a cursos de matemáticas que utilizan Coq se encuentran en Cocorico .

Answer 3

¿Está usted al tanto de la Archivo de pruebas formales para Isabelle? Es una colección de matemáticas formalizadas (y algo de verificación de programas). La lectura de los documentos allí, y navegar por las fuentes de archivos de teoría Isabelle es una buena manera de aprender.

El tutorial de Isar también es un buen lugar para buscar, si quieres escribir pruebas que parezcan matemáticas informales (en oposición al estilo táctico). Es bastante difícil de entender al principio (sobre todo debido a la falta de documentación), pero una vez que lo consigues, es mucho más fácil trabajar con él que con las simples listas de tácticas.

Si quieres formalizar cualquier cosa con aglutinantes de nombres (lambda-calculus, FOL, lenguajes de programación, pi-calculus, etc.) también deberías echar un vistazo al paquete Nominal para Isabelle que, de nuevo, ayuda a abstraer las pruebas.

Answer 4

Me gustaría mencionar Mizar, un sistema de verificación de pruebas basado en un lenguaje legible para el ser humano y muy cercano al lenguaje matemático natural utilizado en la práctica matemática. Es uno de los verificadores de pruebas que más tiempo lleva funcionando, y es uno de los más exitosos. Aquí puedes encontrar algo sobre él: http://www.cs.ru.nl/~freek/mizar/ Toda la biblioteca congaing actualmente más de 40Mb de pruebas comprimidas (¡en puros archivos ascii!).

Answer 5

La mejor introducción al uso de asistentes de pruebas en matemáticas que conozco personalmente es el sitio web de Cameron Freer vdash.org. Ese sitio web también enlaza con algunos recursos, incluyendo las páginas de Freek Wiedijk y John Harrison, que describen brevemente el uso de los asistentes de pruebas en la demostración de enunciados matemáticos.

Por desgracia, la usabilidad de los actuales asistentes de pruebas parece ser extremadamente primitiva, por lo que introducirlos en un curso de posgrado de matemáticas va a ser un reto. Tal vez desee plantear su pregunta al grupo google vdash y/o la lista de correo de la FOM, donde algunos podrían proporcionarle sugerencias útiles o apuntes de conferencias no publicados.