Can computers do math? An approach through axiomatic geometry

The Project

Draw a triangle and divide each of its angles into three equal parts. The rays you just drew are called trisectors, and there are three pairs of adjacent ones intersecting at three different points, thus forming a triangle inside the initial one. One of the most beautiful results of plane geometry states that no matter which triangle you started with, the resulting inside triangle will always be equilateral. Can a computer understand the statement of this theorem? Can it follow a proof that we have? Going even further, if we teach the computer the rules on which we base geometry, will it be able to check that our proof is correct? Will it even be able to find a proof of the theorem by itself?

The axiomatic method, first introduced by Euclid for plane geometry around 300 BC, configured the way we do mathematics nowadays. Since then, more refined and accurate axiomatic systems for geometry have been proposed. In 1899, the great mathematician David Hilbert published Foundations of Geometry, one of the most successful tries. Through Hilbert's five groups of axioms, not only can we formally recover the Euclidean geometry we know, but we can also understand the independence of the parallel postulate (given a line and a point not on it, there is exactly one parallel line through the point) and the rise of non-Euclidean geometries, such as hyperbolic geometry.

On the other hand, recent software like the theorem prover LEAN, launched in 2013, put the power of technology at the service of mathematics. It aims at bridging the gap between a universal errorless framework for formalization and computer-assisted theorem proving. Currently under very active development, what urgently needs to be done is to teach LEAN enough of the mathematics that we "already know" so that it shares our mathematical interests and can try to find new interesting results.

This project aims at teaching LEAN all of Hilbert's axioms, formalizing the proof of basic theorems, and peeking at the use of artificial intelligence. Join us in discovering the past of geometry, the present of computer science, and the future of mathematics.

Learning objectives
  • Describing the axiomatic method in geometry from a historical and mathematical perspective.
  • Implementing Hilbert’s axioms into the programming language LEAN and applying them to formally prove basic geometric theorems.
  • Analyzing the power of theorem provers in formalizing and creating mathematics.
Required materials


Coordinators of the project

Marc Masdeu

  • Number theorist, working at Universitat Autònoma de Barcelona as a Ramón y Cajal researcher. Mainly interested in explicit methods for arithmetic geometry.
  • Obtained M.Sc. in Pure Mathematics at U. Illinois Urbana-Champaign, and Ph.D. at McGill University (Montréal) in 2010.
  • Ritt Assistant Professor at Columbia University (New York, 2010-2013), and postdoctoral researcher at the University of Warwick (Marie Curie Fellow) ) (UK, 2014-2016).
Roberto Rubio

Roberto Rubio

  • BSc in Mathematics, Universitat de València. MSc in Mathematics, Universidad Autónoma de Madrid.
  • Phd in Mathematics, University of Oxford (2015) and Universidad Autónoma de Madrid (2012).
  • Fellow of the United Kingdom Higher Education Academy since 2013.
  • Postdoctoral positions at IMPA (Brazil) and the Weizmann Institute of Science (Israel).
  • Currently, Marie Sklodowska-Curie Individual Fellow at the Universitat Autònoma de Barcelona.
The center

The Department of Mathematics, which is part of the UAB Faculty of Science, is the fundamental structure responsible for organising and developing research and knowledge transfer among its academic staff and its research staff in training. The Department is also responsible for teaching mathematics and statistics in centres, faculties and schools at the UAB, in accordance with their requirements and the teaching programmes in place, and is responsible for organising and developing doctoral and postgraduate programmes and courses.