En fundamentos de las matemáticas, filosofía de las matemáticas y filosofía de la lógica, el formalismo matemático es una teoría que sostiene que las proposiciones de las matemáticas y la lógica pueden considerarse como declaraciones sobre las consecuencias de ciertas reglas de manipulación de símbolos o términos o cadena de caracteres.[1]​[2]​
Por ejemplo, la geometría euclidiana puede ser visto como un juego de lenguaje cuyo objetivo consiste en mover ciertas cadenas de símbolos (llamados axiomas) de acuerdo con un conjunto de reglas llamadas reglas de inferencia para generar nuevas cadenas. En este juego se puede demostrar o probar que el teorema de Pitágoras es válido porque la cadena que representa el teorema de Pitágoras se puede construir usando sólo las reglas establecidas.
De acuerdo con el formalismo, las "verdades" expresadas en la lógica y las matemáticas no son acerca de los números, series, o triángulos o cualquier otra materia específica — de hecho, no son "sobre" nada en absoluto. Son formas sintácticas cuyos contenidos o significados o referencias (ver Sobre el sentido y la referencia) no existen a menos que se les de una interpretación (o semántica).
En la actualidad algunos[3]​ —siguiendo a Michael Resnik[4]​— clasifican el formalismo en "formalismo de juego". "Formalismo de términos" (aquel en el cual los términos (axiomas) solo se denotan a sí mismos y de ellos se deriva proposiciones, pero sin pronunciarse acerca de la realidad ontológica de los mismos; lo que se busca no es prueba de existencia, pero coherencia. etc.
A partir de la década de los 80 del siglo XX, algunos han propuesto que todo nuestro conocimiento matemático formal debe ser sistemáticamente codificados en formatos legibles por un ordenador, a fin de facilitar la comprobación o chequeo automatizadas de las demostraciones matemáticas; la Demostración automática de teoremas y el uso de Demostración interactiva de teoremas en el desarrollo de las teorías matemáticas y programas informáticos. Debido a su estrecha relación con la informática, esta idea también es atractiva a matemáticos logicistas; intuicionistas y constructivistas de la tradición de la "computabilidad"[5]​ (ver también Proyecto Mizar,[6]​ la biblioteca matemática que contiene la colección más grande del mundo de obras matemáticas estrictamente formalizadas y computarizadas.) (pero ver más abajo).
Se ha sugerido que la adopción del punto de vista formalista exime a los matemáticos de la necesidad de preocuparse por cuestiones de los “fundamentos de las matemáticas” y proceder como si estos asuntos hubieran sido resueltos o carecieran de interés matemático. Muchos agregan que, en la práctica, los sistemas axiomáticos que se estudian son sugeridos por las exigencias de la ciencia en cada caso particular.