Prácticamente cada vez que leo la demostración de un teorema en un libro, artículo, diapositivas, página web, pdf, en cualquier sitio, la demostración está escrita utilizando lenguaje natural (por ejemplo, frases en inglés) y a veces dibujos (por ejemplo, dibujos en 2D si se trata de una demostración sobre Geometría, Teoría de Grafos, etc.). Incluso si el autor hace todo lo posible por escribir una demostración muy técnica y formal, llena de símbolos formales, en un momento u otro no puede evitar recurrir al lenguaje natural y/o a los dibujos para transmitir algo. Mi pregunta es: ¿existe un lenguaje formal capaz de expresar cualquier demostración matemática sin recurrir a dibujos o frases en lenguaje natural?
ACTUALIZACIÓN: Como sugirió @Noah Schweber en los comentarios a su respuesta, debería dejar claro que una razón subyacente muy importante de mi interés por las pruebas formales tiene que ver con la cuestión de la confianza en las pruebas en lenguaje natural. Es decir, si no utilizamos ningún lenguaje formal para demostrar la mayoría de los teoremas, ¿cómo podemos estar tan seguros de que hemos demostrado algo? Porque, ¿y si cometemos algún error en algún momento de nuestro razonamiento en lenguaje natural? Puesto que no tenemos una demostración formal simbólica completa, ¿cómo podemos comprobar que nuestra demostración es correcta? Creo que se trata de una preocupación muy válida, teniendo en cuenta que los lenguajes naturales son increíblemente propensos a las ambigüedades, lo que supongo que la mayoría estará de acuerdo en que es una propiedad indeseable cuando queremos demostrar enunciados matemáticos con una certeza cristalina.
