The math seems much improved and it would be a cool trick if it were emulating a symbol processor under the hood. But humans can do that and we opt for calculators and computers for a reason. IMO, the first most useful thing to come from human-machine interface would be adding a highly reliable Turing machine to your cognition.

If we could do that with one of these models, we could have a pretty strong assumption that long proofs and such were performed with strict rules and the model wasn't falling into some going from the gut, "this equation looks like x" type holes. Which seem like a hazard and make me very uncertain any time I see a paper about using ML to come up with answers to what are essentially logical problems.