Something Missing in Euclid? Twenty-Five Centuries of Research Newly Informed by Cornell CS’ Nuprl Proof Assistant

The ongoing Nuprl initiative—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.

Read more