Examples of the value of proofs for algorithms In teaching Intro. Algorithms to undergrads, one of the most difficult tasks is to motivate why they need to know how to prove things about algorithms. (For many students, at least in many US universities, they may see some basic proofs in Discrete Mathematics, but Algorithms is often the first time they have to use proofs to reason about algorithms.) While I think I can do a decent job motivating this at an abstract level, concrete examples are much more convincing, hence my question:


  I'm looking for concrete examples that show the value of proofs in algorithms.


A couple questions already address this, and if you have answers to those, please add them there:


Examples of algorithms and proofs that seem correct, but aren't
How to fool the “try some test cases” heuristic: Algorithms that appear correct, but are actually incorrect


However, I think there are other ways proofs can be valuable beyond the above. E.g., by working through the proof you can gain an insight that leads to a more efficient algorithm, or to an algorithm for a related problem, or to an idea for developing a better test suite to test your implementation, etc.

Some criteria:


Answers here ideally shouldn't fit one of the questions above (as I said, please add an answer there if you have it)
Should be presentable to Intro. Algorithms students. While the proof itself need not be presentable, the story should be presentable (e.g. the statement of the problems involved, some idea of how the proof led to something that just "eyeballing correctness" would not have). If you are unsure about this point, go ahead and add it as an answer and I'll do my best to see if it can be presented to this audience.
Should be as natural as possible. Artificial examples are kinda okay, but real examples are much more motivating to students.
Note that I am talking here about abstract proofs for abstract algorithms, not formal (/automated/etc) proofs of algorithm implementations. As a litmus test, the ideas involved should not be language-specific.


(While this question is not exactly research-level, I think it might get more answers here than on cs.SE, as I suspect the answers will come from  historical examples in the theory of algorithms that expert researchers on this site are more likely to be familiar with.)
Here is a natural problem from graph theory where the proof and the algorithm are closely intertwined. In my view, one can discover this algorithm only via thinking about the proof and the algorithm "in parallel." The task is this:

Input: An undirected graph.

Task: Find a subgraph with maximum edge-connectivity.

Note: What makes the task non-trivial is that a subgraph can have larger edge-connectivity than the whole graph. Since there are exponentially many subgraphs, it would take exponential time to check all of them to find the most connected one, even though we can compute the edge-connectivity of any graph in polynomial time.

Below is a part of a lecture note about solving this problem. It shows that the task can be solved in polynomial time, using a subroutine that finds a minimum cut (which is well know to be doable in polynomial time). For short, edge-connectivity is just called connectivity, and is denoted by $\lambda(G)$.