> Input it into a proof assistant, and rely on the same sort of feedback "does the computer accept your proof, or get stuck". The hard job of formalizing stuff for this purpose has seen significant progress, e.g. by the Lean mathlib project.
As a math teacher who disagrees with the premise of the GGP post ("This couldn’t be more wrong. … I’m sorry, but mathematics is orders of magnitude more intensive and difficult than most programming"), and thinks that any good programmer can learn mathematics—of course there are code wodgers out there who don't really understand their craft of programming, and so can't translate that knowledge to facilitate an understanding of mathematics—I think I also disagree with this. I've never tried it, but I can't imagine someone learning about Stokes's theorem in anything like this way. One of the many axes along which I imagine this failing are that the state of human readability in proof assistants is, well, let's say it's less well developed than the, cough, stellar state of the art in compiler error messages.
But, more importantly, you can, at least in principle, know every single step in a proof of Stokes's theorem without understanding in any real sense why it's true—and a proof assistant in particular will force you into the weeds of minutiae that absolutely do not help to build any intuitive picture—and, even if you manage in the process to piece together that understanding of why it's true, you will never thereby gain an understanding of why it's interesting (e.g., among other things, its connections to physics and the entrée it offers to differential geometry).
The flip side of a proof assistant's 'minutiae' (and there's plenty of room to disagree wrt. whether paying attention to those minutiae helps with gaining a better, more accurate intuition!) is its ease of refactoring a proof. A proof assistant can instantly tell you whether a seemingly nicer, better-abstracted proof B really manages to prove the same thing as proof A, something that's very hard to do without the use of precise formalized statements and automated checking.
As a math teacher who disagrees with the premise of the GGP post ("This couldn’t be more wrong. … I’m sorry, but mathematics is orders of magnitude more intensive and difficult than most programming"), and thinks that any good programmer can learn mathematics—of course there are code wodgers out there who don't really understand their craft of programming, and so can't translate that knowledge to facilitate an understanding of mathematics—I think I also disagree with this. I've never tried it, but I can't imagine someone learning about Stokes's theorem in anything like this way. One of the many axes along which I imagine this failing are that the state of human readability in proof assistants is, well, let's say it's less well developed than the, cough, stellar state of the art in compiler error messages.
But, more importantly, you can, at least in principle, know every single step in a proof of Stokes's theorem without understanding in any real sense why it's true—and a proof assistant in particular will force you into the weeds of minutiae that absolutely do not help to build any intuitive picture—and, even if you manage in the process to piece together that understanding of why it's true, you will never thereby gain an understanding of why it's interesting (e.g., among other things, its connections to physics and the entrée it offers to differential geometry).