arXiv:0810.4315math.LO2008-10-23

A formal system for Euclid's Elements

Jeremy Avigad, Edward Dean, John Mumma

Abstract

We present a formal system, E, which provides a faithful model of the proofs in Euclid's Elements, including the use of diagrammatic reasoning.

Linked by 2 identifiable commenters in 2 comments across 2 threads, from Apr 2010 to May 2019.

Comments linking this paper, per year.

Fancy Euclid's “Elements” in TeX May 20191 comment
- This is a bit random, but there are some formal systems for Euclid's elements out there (see, for example https://arxiv.org/abs/0810.4315). I think it should be possible to implement this in a dependently typed language like Idris, but haven't really worked on this (yet). Any…
  
  meukMay 27, 2019View on HN Parent context
A Formal System for Euclid's Elements Apr 20101 comment
- The Cambridge link appears to be down. Try arXiv instead: http://arxiv.org/pdf/0810.4315v3
  
  jggApr 30, 2010View on HN Parent context

Connected through shared HN threads, not inferred similarity or a recommendation.