Quinn tiene razón en que se puede utilizar la matemática inversa para formalizar la "idea" de una prueba, pero yo añadiría que ésta no es la interpretación o el proyecto habitual de la matemática inversa.
Para responder a tu pregunta, primero tienes que identificar las grandes herramientas, o teoremas, que utilizas en tu demostración. A continuación, se formalizan esos teoremas dentro de la aritmética de segundo orden. El campo de las matemáticas inversas trata de identificar cuándo estos teoremas son equivalentes. Aquí, dos teoremas A y B son equivalentes si se puede demostrar B a partir de A y viceversa, sobre $RCA_0$ . Esto significa simplemente que la prueba B a partir de A también puede utilizar axiomas de la teoría base $RCA_0$ que corresponde aproximadamente a la "matemática computable".
Ahora, puedes formalizar la afirmación "la prueba I y la prueba II son iguales" como la afirmación "los teoremas utilizados en la prueba I son equivalentes a los teoremas utilizados en la prueba II".
En el artículo de la Wikipedia, verás que la mayoría de los teoremas de las matemáticas acaban siendo equivalentes a uno de los cinco subsistemas, cuya fuerza es estrictamente creciente. En otras palabras, la mayoría de las pruebas de un determinado teorema serán equivalentes, o una prueba será más fuerte que la otra.
Por otra parte, investigaciones recientes han demostrado que existe un conjunto mucho más complicado de relaciones entre ciertos teoremas combinatorios débiles. Véase http://www.nd.edu/~ddzhafar/The_Zoo.html para una bonita foto. En este contexto, puedes acabar con dos pruebas no equivalentes del mismo teorema, en las que ninguna de ellas es más fuerte que la otra.
Este fenómeno muestra los teoremas 3 y 5 de un trabajo que acabo de presentar ( disponible aquí ). En este trabajo, doy dos pruebas incomparables de un principio (llamado $RKL$ ). Una prueba utiliza $WKL$ y una prueba utiliza $SRT^2_2$ . Se sabe que estos dos teoremas son incomparables.
Espero que esto ayude.
