# Can an algorithm be part of a proof?

I am an undergraduate student. I have read several papers in graph theory and found something may be strange: an algorithm is part of a proof. In the paper, except the last two sentences, other sentences describe a labeling algorithm.

Can an algorithm be part of a proof? I do not understand why it can be part of a proof. I asked my supervisor but he did not explain it.

LEMMA$\,\,\,\bf 1.$ If $B(G)-b$, then $B(G+e)<2b$.

Proof: Let $f$ be an optimal numbering of $G$, and let $V(G)-\{v_1,\ldots,v_n\}$, numbered so that $f(v_i)-i$. Let $v_lv_m$ be the added edge. We define a new numbering $f'$ such that $|f'(x)-f'(y)|<2|f(x)-f(y)|$, and also $|f'(v_l)-f'(v_m)|-1$. Let $r-\lfloor(l+m)/2\rfloor$, and set $f'(v_r)-1$ and $f'(v_{r+1})-2$. For every other $v_i$ such that $|i-r|<\min\{r-1,n-r\}$, let $f'(v_i)-f'(v_{i+1})+2$ if $i<r$ and $f'(v_i)-f'(v_{i-1})+2$ if $i>r$. This defines $f'$ for all vertices except a set of the form $v_i,\ldots,v_k$ or $v_{n+1-k},\ldots,v_n$, depending on the sign of $r-\lfloor(n+1)/2\rfloor$. In the first case, we assign $f'(v_i)-n+1-i$ for $i<k$; in the second, we assign $f'(v_i)-i$ for $i>n-k$. The renumbering $f'$ numbers the vertices outward from $v_r$ to achieve $|f'(x)-f'(y)|<2|f(x)-f(y)|$. Since we begin midway between $v_l$ and $v_m$, we also have $|f'(v_l)-f'(v_m)|-1$.

• The proof of the Four-Color Theorem is probably the most famous example of proof-by-algorithm.
– user2469
Dec 1, 2013 at 11:53
• I've seen proofs of this kind: To prove that there is an algorithm that solves some problem in polynomial, it is shown that it can be reduced, in polynomial time, to another problem for which there exists a known algorithm that solves it in polynomial time. I'd call the known algorithm part of such a proof.
– user99666
Dec 1, 2013 at 12:18

Yep! Proofs sometimes involve elaborate calculations: presenting an algorithm to do the calculation is a good way to show that the calculation can be done, and to analyze the results of the calculation.

In some fields -- e.g. graph theory -- algorithms are used very frequently. Often, the easiest way to prove that something can be done is to actually write down an algorithm that does it, and prove the algorithm works.

You might think of this approach as a systematic and convenient way to develop and organize complicated inductive proofs. But I would actually think of it the other way: induction is just a rather simplistic kind of algorithm for generating a proof. i.e. the algorithm is "use the argument I called the "base case" to prove it for one $1$, then iteratively apply the argument I called the "inductive step" to prove it for each successive positive integer".

• "Prove the algorithm works" is very, very important. Dec 1, 2013 at 8:04
• Moreover, there is a connection between algorithms and proofs, known as the Curry-Howard correspondence. Dec 1, 2013 at 9:23
• But what is the mathematical definition of an algorithm ? How can it be translated into pure maths (using sequences I guess) ? Is there any rules ? How to be sure the translation of some given algorithm is well constructed ? (Curry-Howard may lead to the answer but........) Dec 4, 2020 at 13:02

I confess that I have not read the paragraph enclosed (which contains some unexplained notation; anyway I am not an expert on graph theory), so this is an answer to your general question.

Absolutely yes an algorithm can be part of a proof. In certain situations (and for those with certain inclinations) an algorithm can be the best possible kind of proof. Let me give a simpler example.

In my linear algebra class recently I told the students that any permutation of $\{1,\ldots,n\}$ can be obtained as a composition of transpositions -- i.e., swapping two elements at a time. This is not an obvious fact if you haven't thought about it before. What was my proof? Well, I said that in fact you can choose the transpositions to be adjacent elements, and then I told the students that the easiest way to see this is to think about how to actually do it in practice. It is easy to give an algorithm: start with the element that you want to go in the $n$th place. If it's there already, great. If it isn't, then keep making a sequence of adjacent swaps bringing it one step closer to the $n$th position every time. Do this until it gets into the $n$th position. Now we can view what we have left as a permutation of $\{1,\ldots,n-1\}$ and work by induction.

The above argument is definitely an algorithm: it is something that a CS student would have little trouble programming. And it is a convincing proof. What's convincing about it of course is that you can see why the algorithm is doing what it's supposed to do. We could write it more formally if we wanted to, as a global induction argument, and then we could use the well-ordering principle to argue that moving the element one step closer each time to where it wants to go means that it will eventually get there, but that seems like overkill in the present case.

In summary: an algorithm can definitely be part of a proof, but except for completely trivial cases an algorithm -- written in the form that a computer would accept, for instance -- should not be the entirety of the proof. The other important part is an explanation for why the algorithm is doing what it is claimed to do. Sometimes that's simple; sometimes it isn't. There are in fact some amazing theorems that say (roughly) in general it is impossible to figure out what an algorithm will do, so the algorithms that are part of proofs need to be of the relatively simple kind whose workings can be explained to a human being.

Afterthought: By the way, "When is an algorithmic proof preferred and when is a pure thought/existence proof preferred?" would be a fantastic question, in my opinion.

• Hi, could you write it more formally ? I am not sure all math students know how to write it formally and it could be a good exercise to practice mathematical reasoning. Moreover, I am looking for a method (rules or something) to translate this kind of algorithms into more formal math, do u have any idea or references ? Thank u for your consideration Dec 4, 2020 at 13:09

The proof shows how to renumber the vertices with the integers $1,\ldots,n$ in such a way that $|f\,'(v_\ell)-f\,'(v_m)|=1$, where $e=v_\ell v_m$ is the new edge, and $$|f\,'(x)-f\,'(y)|\le 2|f(x)-f(y)|$$ for each edge $xy$ of $G$. You have to think through the construction to see that it actually does this, but that’s not too hard to do. This shows that $G+e$ has a numbering $f\,'$ such that

$$\max_{xy\in E(G)\cup\{e\}}|f\,'(x)-f\,'(y)|\le 2\max_{xy\in E(G)}|f(x)-f(y)|\;,\tag{1}$$

where $E(G)$ is the set of edges of $G$.

I assume from the context that $B(G)$ is the minimum over all numberings $g$ of $$\max_{xy\in E(G)}|g(x)-g(y)|\;;$$ $f$ is a numbering that achieves this minimum. Thus, $(1)$ shows that $G+e$ has a numbering $f\,'$ such that

$$\max_{xy\in E(G)\cup\{e\}}|f\,'(x)-f\,'(y)|\le 2B(G)\;.$$

It follows that if $f''$ is an optimal numbering, meaning one that achieves the minimum possible value of

$$\max_{xy\in E(G)\cup\{e\}}|g(x)-g(y)|\;,$$

then

$$B(G+e)=\max_{xy\in E(G)\cup\{e\}}|f''(x)-f''(y)|\le \max_{xy\in E(G)\cup\{e\}}|f\,'(x)-f\,'(y)|\le 2B(G)\;,$$

which is what the lemma claims.

It’s true that this renumbering scheme can be thought of as an algorithm, but that’s really beside the point: the real point is that it makes clear to the reader why the lemma is true, which is precisely what a proof is supposed to do. It’s also true that just describing the scheme doesn’t fill in all of the details of the proof; as I said, you still have to convince yourself that it works as stated. But that’s true of all proofs outside of the very limited realm of formal theorem-proving: you always have to fill in some of the details for yourself.

• wow this is brilliant. Thank you Brian! (+1) Dec 1, 2013 at 4:02
• @DonAnselmo: You’re welcome! Dec 1, 2013 at 4:04
• Hi @BrianM.Scott, I am looking for a method (rules or something) to translate any kind of algorithms used in proof into more formal math, do u have any idea ? Do you think the way to translate it into formal math is case specific ? How to be sure our translation is true ? (for instance, how do you know the formal proof you have given is the true translation of the algorithm?) Thank u for your consideration Dec 4, 2020 at 13:13
• @RémyHosseinkhanBoucher: I don’t, I’m afraid. To be honest, I’ve never had much interest in formal proofs; to me the important thing is to describe the reasoning clearly enough that others can follow it and judge its correctness for themselves. Dec 4, 2020 at 18:20

Here is a short answer to the question in your title. Typically, when one gives a constructive proof, in essence, the constructive argument forms the algorithm. An example that comes to my mind is again from combinatorics: Stable marriage theorem. The easiest way to prove the existence of a stable marriage is to provide an algorithm to construct one.

• +1, I was going to give this exact same example myself. Dec 1, 2013 at 15:41
• Of course, just the fact that a proof is constructive doesn't necessarily mean it results in an efficient algorithm. One example: given $n$ distinct points in the plane, there exists an ordering such that the cycle has no intersection between its edges (other than the obvious ones at vertices). Proof: a "travelling salesman" permutation which minimizes the total length of the cycle must work - otherwise, if there's a crossing, you can reverse a part of the cycle to make the total length shorter. But since there's no known efficient solution to the travelling salesman problem, Jun 1, 2017 at 0:46
• the algorithm directly translated from the proof isn't going to be efficient. (On the other hand, you can construct an algorithm which goes through and sees when the reversal operation can make things shorter, and iterates until it finds no such reversal. That algorithm, at least in practice, seems to have reasonably good runtime performance.) Jun 1, 2017 at 0:48

By the Curry-Howard correspondence, any logical proposition in intuitionistic logic can be taken as the type signature of a lambda calculus expression. Equivalently one might use combinators rather than lambdas, and have one combinator corresponding to each logical axiom or inference rule.

Lambda calculus with types is powerful enough to be a real programming language; indeed there are several programming languages in use today which are little more than lambda calculus with additional types such as machine integers and efficient data structures, and a healthy dose of syntactic sugar.

Lambda calculus is also turing complete, meaning you can use a turing machine for a proof of a logical statement too.

Therefore, an algorithm (which has been proven correct) is a proof.

If you ask me, I would say that everything can be part of a proof as long as you bring a convincing reasonable argument. When I listen to my colleagues topologist, they make a few drawings (generally sketches of knots) on the blackboard and they claim it's a proof. Thus, a drawing or an algorithm, there is no big difference, the most important at the end of the day is that you are sure of what you assert, and leave nothing in the darkness.

Have a nice day :-)