Respuestas
Demostraciones formales e informales
Dentro de la teoría de la demostración es muy importante distinguir entre las demostraciones «informales» encontradas en la práctica cotidiana de los matemáticos y en los libros comunes sobre matemáticas, de las demostraciones puramente «formales» de la teoría de la demostración formal. Las primeras tienen el objetivo de mostrar rigurosamente un resultado matemático de manera clara, pero al mismo tiempo intuitiva e inteligible, las segundas de estas demostraciones son como una especie de esquemas de alto-nivel escritos en lenguaje formal, que en principio, pueden permitir a un experto o un lógico construir una demostración puramente formal del mismo resultado, dado el suficiente tiempo y paciencia. Para la mayoría de los matemáticos, escribir una demostración completamente formal es demasiado pedante y un gasto de tiempo innecesario como para ser práctica común.
Las demostraciones formales pueden ser construidas con ayuda de ordenadores mediante métodos de demostración de teoremas interactivos u otras técnicas. Es significativo, que estas demostraciones puramente formales basadas en la manipulación de signos pueden ser verificadas automáticamente, también por ordenador. Verificar una demostración puramente formal es simple, mientras que encontrar demostraciones es generalmente mucho más difícil. Una demostración informal en un artículo matemático, por el contrario, requiere semanas de revisión por pares para ser verificada, y frecuentemente puede contener errores que pasen inadvertidos incluso para matemáticos profesionales en temas de investigación suficientemente complejos.
La teoría de la demostración formal se ocupa de las propiedades de los sistemas deductivos, su complejidad, el poder expresivo de dichos sistemas y está íntimamente conectada a la lógica matemática, la teoría de modelos y la fundamentación de las matemáticas. Por el contrario el desarrollo de demostraciones informales es un terreno altamente creativo y si bien existen familias enteras de esquemas de demostración en diferentes áreas, son un ejercicio básicamente humano en el que no existen algoritmos generales para construir demostraciones.