I'm surprised not to see any mention yet of constructive type theory and computer proof assistants, in which a computer program is literally a proof and vice versa. For instance, if you wrote a program to compute the result of the Collatz function in a verified and termination-checked programming language like Coq or Agda, then it would be a proof of the Collatz conjecture. Conversely, a proof of the existence of an object in constructive type theory is, literally, an algorithm to compute that object.

I think computers have many roles to play in mathematics education. The coding of algorithms certainly has a place in education, but it seems to me that a more promising way to use computers to teach logical reasoning is to use a computer program that actually understands logical reasoning. Hence why I asked this question.

I'm surprised not to see any mention yet of constructive type theory and computer proof assistants, in which a computer program is literally a proof and vice versa. For instance, if you wrote a program to compute the result of the Collatz function in a verified and termination-checked programming language like Coq or Agda, then it would be a proof of the Collatz conjecture. Conversely, a proof of the existence of an object in constructive type theory is, literally, an algorithm to compute that object.

I think computers have many roles to play in mathematics education. The coding of algorithms certainly has a place in education, but it seems to me that a more promising way to use computers to teach logical reasoning is to use a computer program that actually understands logical reasoning. Hence why I asked this question.