From my understanding, for proofs to be considered "formal" as opposed to social/casual, they need to be computable or at least be a set of transformations of strings of symbols. By algorithm I mean step-by-step transformation, along the lines of the Curry-Howard correspondence (programs are proofs).
In looking for a reasonably long social proof, I found the example at the bottom. It's proposition is simple, just one line. A function is a bijection between two structures, and the two structures are related to the functions input and output. It's proof is long though. It has a lot of pieces. But it seems like if enough work was put into it, it could be converted to an algorithm.
I'm wondering the following:
- The general strategy of how one would make this into a valid formal proof. Doesn't need to be for this specific example which has some background knowledge in the paper.
- If algorithms are proofs. If not, why not.
- If algorithms could constitute a valid formal proof in some way.
Wondering if simply an algorithm showing a transformation of $a$ into $b$ and $b$ into $a$ would be enough. This confuses me because theoretically you can construct any algorithm to convert anything into anything else. Convert an integer into a float, just add a decimal point. Convert an integer into a sheet of paper, just stretch the integer into a square. Convert a donut into a coffee cup, etc.
So if a proof (proof theory) is just a translation from $a$ to $b$, then there are what seems like an infinite array of possibilities for doing the formal proof. One possibility of proving the cup/donut are "equivalent" in some way is to show the animation above. Maybe there are others.
Other "automatic" proofs like the donut example might be:
- Translation of text from one language to another (algorithm for each character or word or whatnot). Wondering if it is a "proof".
So wondering what counts as a valid formal proof. Wondering if it can just be an algorithm that stretches and morphs something into the other thing. Or if it needs to be more formal/standardized than that. The reason algorithms are appealing is because it is easy to comprehend. But wondering if it is enough to to have an algorithm in place of a proof.
Proposition 1 (Pointed graphs modulo and path structures isomorphism). The function $\tilde{P} \mapsto X(\tilde{P})$ is a bijection between $\tilde{P}_\pi$ and $X(\tilde{P}_\pi)$.
Proof. [Surjectivity]. By definition of $X(\tilde{P}_\pi)$. [Injectivity]. Let us suppose that $X(\tilde{P}) = X(\tilde{Q})$. Then $\equiv_\tilde{P}$ and $\equiv_\tilde{Q}$ must have the same number of equivalence classes and $|V (\tilde{P})| = |V (\tilde{Q})|$. Let us choose two graphs $P \in \tilde{P}$ and $Q \in \tilde{Q}$. For any vertex $u$ of $P$, there is a unique equivalence class $c$ of $\equiv_\tilde{P}$ such that the paths of $c$ lead to $u$ in $P$. Since $\equiv_\tilde{P}$ and $\equiv_\tilde{Q}$ are supposed equal, $c$ is also an equivalence class of $\equiv_\tilde{Q}$. Conversely given $c$ an equivalence class of $\equiv_\tilde{Q}$, there is a unique $v$ of $Q$ such that the paths of $c$ lead to $v$ in $Q$. Then, the paths which point to $u$ in $P$ are the same as those which point to $v$ in $Q$. We can now define a function $R$ which maps each vertex $u$ in $P$ to its corresponding vertex $v$ in $Q$. Because this is a bijection, we can then extend $R$ to be a bijection over the entire set $V$. Let us consider two vertices $u$ and $u'$ in $P$ linked by and edge $\{u : i, u': j\}$ and their corresponding vertices $v$ and $v'$ in $Q$. As $P \in \tilde{P}$, we have that the equivalence classes $\tilde{u}.ij = \tilde{u'}$ . As the classes representing $v$ and $v'$ are equal to $\tilde{u}.ij$ and $\tilde{u'}$ . Thus $R$ is a graph isomorphism, and $P$ and $Q$ are isomorphic. This is true for every $P \in \tilde{P}$ and $Q \in \tilde{Q}$ thus $\tilde{P} = \tilde{Q}$.
A formal mathematical proof is a sequence of logical statements which starts with self-evident or assumed statements (known as axioms) and ends with the statement to be proved, and in which each statement in the sequence is a consequence of the previous statements in the sequence using accepted rules of logical inference.
A formal proof is not itself an algorithm (although it may involve the construction or application or algorithms). However, there is an algorithm to check the correctness of a proposed proof - one of the profound insights of Kurt Gödel was that a formal proof can be encoded as a sequence of integers, and checking the correctness of the proof can be reduced to checking arithmetical properties of these integers.
Having said that, mathematicians do not usually write out the full details of a formal proof. Neither do they use a proof checking algorithm to validate proofs written by other mathematicians. Instead, mathematicians usually write "semi-formal" proofs which start from known results instead of axioms, and which provide an outline of how a formal proof could be constructed. The proof of Proposition 1 that you quote at the end of your question is an example of a semi-formal proof - if it was written out as a formal proof, it would be much longer.
Finally, I don't agree with your assertion that theoretically you can construct an algorithm to transform anything into anything else. Using your example, how would you transform an integer into a sheet of paper ? Just considered as sets, they have (very) different sizes. You can transform an integer into one point on the sheet of paper, but how do you map a single integer to every point on the sheet of paper at the same time ?