Luca Ferranti

This talk introduces [GeometricTheoremProver.jl](https://github.com/lucaferranti/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](https://github.com/lucaferranti/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.

Luca Ferranti

Talks:

Automated Geometric Theorem Proving in Julia

Platinum sponsors

Gold sponsors

Silver sponsors

Media partners

Community partners

Fiscal Sponsor