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.
