Modern Mechanized Mathematics

Jacques Carrette

Doing mathematics by computer is divided into two camps: numerical analysis and symbolic computation, both with very different flavors. Strangely, symbolic computation itself has split into two: theorem proving and algebraic (exact) computation. These two have developed largely independently for the last 40 years [yes, that long]. But there is a subset of these two communities who are striving to merge these two strands. Along with William M. Farmer, we are implementing a new system which gives equal weight to proofs and computation. Unlike our communities of origin, we value both correctness and efficiency equally. We are now using modern techniques (partial evaluation, dependent types, abstract interpretation, generative programming, etc) to implement a new system.

Another facet which we are actively exploring is the mismatch between the ``mathematics process'' and current tool support. While most parts of the mathematics process have corresponding tools, no tool comes even close to offering a reasonable environment for ``doing mathematics''. I have two particular application areas which I use for requirements analysis: (formal) software engineering and mathematical analysis (i.e. calculus). From my experience, these are two areas where new tools could have a large impact.