¿Puedes usar lógica pura para probar una conjetura matemática?

Un tema fundamental bastante amplio, por lo que me referiré a WP para obtener breves descripciones accesibles.

La lógica formal y las matemáticas comparten muchos aspectos en el pensamiento humano. Ambos están fuertemente influenciados por la notación disponible, que parece informar el pensamiento intuitivo. Sin un pensamiento intuitivo, el progreso está muy atrofiado, pero, por supuesto, la intuición puede resultar errónea.
Prefiero el trabajo sobre esquemas de axiomas, algunos de los cuales involucran patrones en lugar de cadenas de letras (WP tiene un esquema de página Axiom no particularmente bueno).
Sospecho que no todos los problemas son fácilmente expresables o incluso solucionables como las cadenas unidimensionales convencionales a las que estamos acostumbrados en nuestra expresión general, lo que abriría la puerta a las matemáticas que no están abarcadas por la lógica, y la lógica que no es expresable matemáticamente. Eso puede ser algo para otro siglo.

Las personas de mi generación tienden a pensar en el horario de Hilbert (programa de Hilbert), una serie de problemas difíciles destinados a establecer el conjunto de las matemáticas sobre una base lógica firme y completa, y luego de la saga de
Principia Mathematica necesita ser reescrita, y al aprobar los teoremas de incompletitud de Gödel que mostraron que algunos de los objetivos del programa de Hilbert son imposibles.

El área temática se conoce como Fundamentos de las matemáticas.

Creo que estoy en lo cierto al decir que el trabajo más actual en el área tiene que ver con la teoría de la Prueba, pasando a problemas de computación y computabilidad, si existen algoritmos que podrían resolver problemas difíciles de manera confiable dentro de un tiempo razonable (es decir, antes del final proyectado del universo), una forma de desarrollo de problemas de existencia.

Si puede resolver el problema P versus NP antes de los 40 años, definitivamente obtendrá una medalla Fields. Sin embargo, puede llevar bastante tiempo al matemático promedio comprender cuál es el problema.

¿Qué significa “lógica pura” aquí? Si todo lo que se nos permite usar es, digamos, razonamiento proposicional o propiedades de la lógica de primer orden que son independientes del modelo subyacente, hay poco interesante que se pueda decir.

¿Podemos demostrar un teorema interesante sobre las estructuras algebraicas sin usar las propiedades de las estructuras algebraicas? Ciertamente podemos probar teoremas como

Si G es un grupo conmutativo, entonces G es un grupo

por simple eliminación de conjunción pero ¿son interesantes los teoremas de esta forma? No en mi opinión

Hay mucho trabajo en formalizar y verificar teoremas utilizando asistentes de prueba como Coq e Isabelle, pero en todo este trabajo uno tiene que formalizar las propiedades del dominio matemático que le interesa al definir las propiedades de las entidades involucradas.