The cynists will comment that I've just been sucked in by the PR. However, I know this team and have been using these techniques for other problems. I know they are so close to a computationally-assisted proof of counterexample that it is virtually inevitable at this point. If they don't do it, I'm pretty sure I could take a handful of people and a few years and do it myself. Mostly a lot of interval arithmetic with a final application of Schauder that remains; tedious and time-consuming, but not overly challenging compared to the parts already done.
The cynists will comment that I've just been sucked in by the PR. However, I know this team and have been using these techniques for other problems. I know they are so close to a computationally-assisted proof of counterexample that it is virtually inevitable at this point. If they don't do it, I'm pretty sure I could take a handful of people and a few years and do it myself. Mostly a lot of interval arithmetic with a final application of Schauder that remains; tedious and time-consuming, but not overly challenging compared to the parts already done.