Very interesting. I’m actually the most struck by the potential that this system might offer for math education, with its human-readable and human-like proofs. Math games have so far been focused on teaching how to do relatively mechanical things like arithmetic and algebraic manipulation because it’s easy to automatically verify the correctness of those, but maybe something like this could be used to teach the creative side of mathematics as well? Let the student dabble around with various kinds of proofs, and let the system tell them which ones are correct, and provide guidance if the student is stuck.
Very interesting. I’m actually the most struck by the potential that this system might offer for math education, with its human-readable and human-like proofs. Math games have so far been focused on teaching how to do relatively mechanical things like arithmetic and algebraic manipulation because it’s easy to automatically verify the correctness of those, but maybe something like this could be used to teach the creative side of mathematics as well? Let the student dabble around with various kinds of proofs, and let the system tell them which ones are correct, and provide guidance if the student is stuck.