Quietly located in a small space in Gates Hall, the ongoing Nuprl initiative (pronounced “new pearl”)—that implements computational mathematics by providing logic-based tools for program automation—is turning up some surprising and significant results. In conversation with Robert Constable, Professor of Computer Science and founding dean of CIS (who joined the faculty in 1968), and Ariel Kellison, a research support specialist for Nuprl, it was revealed that Kellison had discovered something missing in Euclid’s work. The vagueness of the “something” is meant to register both a mathematicians’ scientific caution and the fact that sometimes an elision in a great work is not a mistake. Still, something has been missing . . . until now.

Kellison said the discovery arose while “formalizing synthetic spaces” using the Nuprl proof assistant: “In the Nuprl group we are simultaneously researching (as separate projects) both the earliest and most modern accounts of synthetic spaces. The earliest account of synthetic spaces is geometry in the style of Euclid. In Euclid’s geometry, points, lines, angles, and circles can be constructed, described, and reasoned about without any notion of a number system. This constituted the practice of geometry before Descartes’ ‘arithmetization’ of space. Similarly, a modern account of synthetic spaces is given by homotopy type theory, where notions such as paths between spaces can be reasoned about directly without needing to be defined (analytically) in terms of a set of points.”

People familiar with geometry will appreciate that it is a practice for understanding space and the relationships within space. But with “synthetic spaces,” new possibilities for proving theorems are afforded, especially by way of “synthetic mathematics” (a domain contrasted with analytic mathematics and its reliance on real numbers). Kellison provides a useful example: “while Euclidean geometry has a model in the Cartesian plane, omission of only one of the synthetic axioms, the parallel postulate, admits models that are valid in the hyperbolic plane as well.”

So what precisely might be “missing” in Euclid? In Kellison’s reply to the question, she sketches the history of engagement with Euclid’s field-defining book, the Elements and where Nuprl has led the team: “It is well known that the straightedge and compass constructions in the Elementsonly show that a proposition holds for a specific configuration of points, even though the proposition is stated in general, meaning it should hold for all possible configurations. We would like show that general proofs for these basic theorems of geometry can be given using the traditional tools of the geometer, such as the straightedge and compass.”

Looking further into recent discoveries of Nuprl research into “synthetic geometry,” Kellison—with a team of researchers, including lead scientist Mark Bickford and chief programmer Richard Eaton—has recently shown in the Nuprl proof assistant that the second proposition from Book I of the Elements of Euclid can be demonstrated generally using a functional interpretation of the traditional tools of the geometer [See note 1 below]. This outcome is contrary to all accounts given for the last twenty-five centuries, which claim that no general straightedge and compass construction for Euclid’s second proposition exists.

Not to be overlooked is the way these insights into synthetic mathematics relate to the domain of homotopy type theory, an area for which Bickford has contributed a model of cubical type theory in the Nuprl proof assistant [See note 2 below]. His work gives rigorous insight into the foundations of this new and exciting area of mathematics.

Kellison has discovered other “missing pieces” in Euclid, which we will discuss in future updates about her work and research conducted by the Nuprl lab in the Cornell CS department. For now, though, we are treated to the uncanny sense that after more than two-and-a-half-millennia, we are company to a novel discovery in Euclidean geometry.

References

[1]  Ariel Kellison, Mark Bickford, and Robert Constable. Implementing Euclid’s Straightedge and Compass Constructions in Type Theory. Annals of Mathematics and Artificial Intelligence, September 2018.

[2]  Mark Bickford. Formalizing category theory and presheaf models of type theory in nuprl. Technical Report arXiv:1806.06114v1v1, CS.LO 15 June 2018, 2018.