Esta pregunta está relacionada con la (tal vez incluso de la misma en la intención) Pregunta 1017, pero ninguna de las respuestas parecen frente a lo que yo estoy buscando.
Hay un montón de recursos disponibles para las personas que quieren utilizar la prueba como asistentes, Coq, Isabelle, ..., para demostrar propiedades sobre los programas—y que no es ninguna sorpresa, ya que mucho del desarrollo de estos programas es realizada por científicos de la computación. Sin embargo, estoy interesado en los recursos, y especialmente en los materiales del curso (porque estoy tratando de armar un estudio independiente de un estudiante de CS), que implica el uso de la prueba de los asistentes para demostrar matemática declaraciones—ver la obra de Hales y Weedijk para los ejemplos. ¿Alguien sabe de algún ejemplo?