Can computers do math? An approach through axiomatic geometry
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.
- 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.
Laptop
