Fine. Express the homological proof of the Brouwer fixed-point theorem on a computer. Ideally in a way that is easily understood by both a computer and a mat

Fine. Express the homological proof of the Brouwer fixed-point theorem on a computer. Ideally in a way that is easily understood by both a computer and a mathematician. Bonus points if it can be used as a teaching tool, too, so that a (sufficiently mature) math student could read it and follow the proof. Assuming you agree the above is Really Hard™, then we've established there's an upper limit on how effective computerized math education can be (for now). This leads to a bunch of interesting questions. Where is that limit? Can we design a computerized version that satisfies the design requirements for that system? Do we have the technology to make it happen? Is it even a technology problem to begin with? Yabba dabba doo.