This is the exact attitude that the blog post is saying is wrong. For mathematics, computers are tools. Computers don't create the answers, they assist the user in finding the answer. They're time-saving and error checking devices, which are useful after the student learns the concepts inside and out. They are not supposed to solve the problems directly.

>>"Explain whether 4/3 or 3/4 is closer to 1, and how you know."

>I am not familiar with the domain, but dont we have some automatic theorem-proving tools? This would look like a perfect use case to me.

Theorem proving tools would work if the students wrote their answers in a format that the tool would work in. In this case, it would be a natural language proof instead of a formal proof, which simply isn't possible to parse right now. Perhaps it will be in the future.