Quite a nice result. Along the lines of your point 2., it's not the first time in recent years a problem in operator algebras was resolved by the computer science community using unexpected methods: https://www.quantamagazine.org/computer-scientists-solve-kad.... Perhaps looking at these problems from a more concrete angle is the way to go, especially for a problem like disproving the Connes conjecture.