On the Role of OpenMath in Interactive Mathematical Documents

The standard OpenMath is an enabling technology for creating an integrated computer environment in which software packages for computer algebra and for proof checking can be combined. Here we demonstrate how OpenMath can be employed for generating interactive mathematical documents containing primality proofs. Our case study takes place within a browser; once a prime number is specified, a document appears summarizing the proof in a number of assertions. By clicking an assertion regarding the truth of an arithmetic equality, a computer algebra calculation is invoked verifying the equality. By clicking an assertion regarding a specific mathematical lemma called Pocklington’s Criterion, a verification of the corresponding formal proof is carried out by a proof checker. Moreover, the whole document is structured in such a way that it can be easily translated to a formal proof object. OpenMath supports the interaction between the document as it appears in the browser and the mathematical software packages. This paper begins with an introduction to OpenMath and a brief comparison with MathML.