A Framework for an Art History of Proofs#

Author: Steve Kieffer

Every art form has a history. Styles and techniques evolve, practicioners introduce new ideas, conventions rise and fall. By studying these histories we enhance our appreciation of individual works of art, by learning to see each as occupying a place within a continuum.

Like pieces of music or chess games, mathematical proofs constitute an art form deserving of focused historical studies. Such studies could be enhanced by a specialized, common framework in which to represent proofs.

Common frameworks#

If we wish to study and compare great works of classical music, by masters like Bach, Mozart, Beethoven, or Chopin, we have a fixed, common framework in which to do this. Music is recorded in a standard notation on music staves. Using this, an historian might be able to point out the very first time the key was modulated by progressing from the tonic chord to a dominant III, followed by a minor VI. Perhaps it happened in the seventh bar of the second movement of such and such quartet by so and so….

If we wish to study and compare great chess games of the past, by masters like Lasker, Capablanca, Fischer, or Kasparov, we have a fixed, common framework in which to do this. Each move in a game is described by a symbolic expression such as “e4” or “Nxc6”. And each move is numbered, so that a particularly brilliant and memorable move may be cited, e.g. the queen sacrifice on move 23, in the third game of tournament such and such….

If we wish to study and compare the great proofs of mathematics, what common framework do we have? How do we point to the steps of proofs? Better yet, can we link to the steps of proofs?

Proofscape and libpaths#

The Proofscape argument mapping system offers a simple way of building a database of proofs, so that every proof step has a unique address, called a libpath (short for “library path”).

For example, if you want to point to one of the clever constructions that made the original proof of Hilbert 90 work, you’ll find that it lives here:

gh.alpinemath.histarch.H.ilbert.ZB.Thm90.Pf.I02

and that you can provide a link to this step.

The first three segments of a libpath are the host, owner, and repo segments. In the example above, these three segments indicate that this node is found in the histarch repo owned by the alpinemath organization at GitHub.

All subsequent segments of a libpath denote Proofscape entities within the repo. In the case above, each of H, ilbert, ZB, and Thm90 denotes a Proofscape module, while Pf denotes a deduction (a proof), in which there is a node called I02.

Conclusions#

The The Historical Proofs Archive project makes the beginning of a fixed, common framework in which to communicate insights, observations, and questions. Now, like moves in chess games, and beats and measures on music staves, every step in every proof of historical interest can be referenced in a precise way, opening the door to an exciting new art history of proofs.