I don't know if it's precisely the same thing, but invariants in the form of conservation laws are quite handy in physics too. They let you take problems with complicated details and turn them into accounting problems. One of my favorites is the optical invariant, which relates the area and divergence of a light beam. It provides a way to work through problems very quickly, say, during a meeting or when considering design options.
Invariants are always useful! They were a major software engineering innovation in the 80s with languages such as Eiffel, and Lamport for example suggests teaching concurrency in terms of invariants (for example, conditions that must be respected at the end of all mutual exclusive sections).
There is actually a connection with physics, although the invariants are properties of particular quantum field theories.
It's the basis for topological quantum computing.
I'm not sure about the severity of its impact, but I toyed with the problem when I was learning knot theory. It's a spot where probably hundreds of mathematicians have tried to itch. Advances have been made in attempts to solve it, but didn't quite do the job. Piccirillo's approach is really quite beautiful, and... sorry, this is where mathematics gets weird: the statement of the theorem is what lay-people consume; the method of proof (not even the actual proof, but the ludicrously high-level abstract algorithm that the proof is a concrete instance of) is what mathematicians consume. In that regard, this seems quite buzzworthy.
But if you're a fan of mathematics but still consider yourself a lay person: this stumped John Conway!
This is why computer based proofs aren't interesting to mathematicians. There is some small amount of value in proving results, but the real value is the new techniques people came up with to prove novel results. As you call it the "high-level abstract algorithm".
Those provide new tools for proving other results and directions for study. A computer based proof will probably just be an incomprehensible mess, think something like an evolved neural net. Not helpful at all.
I don't know about a source, but Conway had been compiling knot tables since high school, and as a knot with only 11 crossings, the Conway knot is certain to have been on his radar. It's just such a simple knot, and sliceness such a fundamental property that Conway is sure to have tried to figure it out.
You've caught me there. I'm having trouble even locating a source for why it's even called the Conway knot! The wolfram page has a few references of about the right age, but I don't have access to them, sadly. It being a long-standing question about a knot named after him, I'm fairly certain that he'd take a crack at it. But alas, that's no proof.
