[Axiom-developer] Computational Math and Terence Tao's three stages of mathematics

[Tim Daly]

https://terrytao.wordpress.com/career-advice/there%E2%80%99s-more-to-mathematics-than-rigour-and-proofs/

One can roughly divide mathematical education into three stages:

1. The “pre-rigorous” stage, in which mathematics is taught in an informal, intuitive manner, based on examples, fuzzy notions, and hand-waving. (For instance, calculus is usually first introduced in terms of slopes, areas, rates of change, and so forth.) The emphasis is more on computation than on theory. This stage generally lasts until the early undergraduate years.
2. The “rigorous” stage, in which one is now taught that in order to do maths “properly”, one needs to work and think in a much more precise and formal manner (e.g. re-doing calculus by using epsilons and deltas all over the place). The emphasis is now primarily on theory; and one is expected to be able to comfortably manipulate abstract mathematical objects without focusing too much on what such objects actually “mean”. This stage usually occupies the later undergraduate and early graduate years.
3. The “post-rigorous” stage, in which one has grown comfortable with all the rigorous foundations of one’s chosen field, and is now ready to revisit and refine one’s pre-rigorous intuition on the subject, but this time with the intuition solidly buttressed by rigorous theory. (For instance, in this stage one would be able to quickly and accurately perform computations in vector calculus by using analogies with scalar calculus, or informal and semi-rigorous use of infinitesimals, big-O notation, and so forth, and be able to convert all such calculations into a rigorous argument whenever required.) The emphasis is now on applications, intuition, and the “big picture”. This stage usually occupies the late graduate years and beyond.

I'm of the opinion that computational mathematics is at the first stage. We write

code that "sort-of works" and lacks any attempt at formality, even failing to

provide literature references. Moving to stage 2 will be a long and tedious

task. Axiom has the connections to the proof machinery and is being

decorated to provide some early attempts at proofs using ACL2 and COQ.

This effort is an interesting combination of mathematical proof and

computational proof since both fields underlie the implementation.

Moving computational mathematics up Tao's tower is going to be a long, slow,

painul effort but, if memory serves me correctly, so was graduate school.

Tim