Automated Geometric Theorem Proving in Julia

This talk introduces GeometricTheoremProver.jl, a Julia package for automated deduction in Euclidean geometry. The talk will give a short overview of geometric theorem proving concepts and hands-on demos on how to use the package to write and prove statements in Euclidean geometry. A roadmap of the package for future development plans will also be presented.

Geometry has been central in formal reasoning, with Euclid's Elements being the first example of axiomatic system. Centuries later, Euclidean geometry is still central e.g. in mathematical education as introduction to formal proofs. To make things more exciting, Tarski proved in early 1900 that Euclidean geometry is decidable, that is a computer program should be able to answer questions like "is this statement true?". This opened several interesting questions: How can I prove efficiently statements in Euclidean geometry? Can I generate readable proofs? During the talk, I will touch those questions while introducing GeometricTheoremProver.jl, a package for automated reasoning in Euclidean geometry written fully in Julia. The talk will combine a short overview of geometric theorem proving concepts with hands-on demos on how to use the package to write and prove statements in Euclidean geometry. Finally, the talk will also present a roadmap for the package, hopefully giving pointers to the interested listener on how to contribute.