Need feedback : Euclid and Hilbert

Stream: general

[Vaibhav Karve]

I would like to introduce the Lean community to 4 new members:

• Lawrence Zhao
• Edward Kong
• @Alex Dolcos
• Nicholas Phillips

They are high-school students (making them some of the youngest members of our community :slight_smile: ).

They have been working with me over the past month on a summer research project (as part of a program run by the department of math
at University of Illinois at Urbana Champaign). I myself am a graduate student and had some previous experience with Lean but for Lawrence, Ed, Alex and Nic, this is their first foray into theorem-proving territory. I was delightfully surprised by how quickly they were able to warm up to Lean and were able to make substantial progress in such a short time.

We are excited to share the results of our labor here. We have attempted formalizing Euclid's and Hilbert's Geometry axioms in Lean and are looking for any feebback that the comminuty can offer us on how to improve things. We have proved some lemmas and propositions but a lot
more needs to be done. Our goal is to formalize all 48 of Euclid's propositions (including the Pythagorean theorem) in Lean.

We called our project LeanTeach2020. Link to code repo -- https://github.com/vaibhavkarve/leanteach2020

[Kevin Buzzard]

What's the story with the sorrys in tarski.lean -- are they also axioms or should they be fillable?

[Patrick Massot]

How does it interact with Ali's stuff?

[Kevin Buzzard]

Ali used variables not constants, and he probably proved more but he only did Tarski

[Vaibhav Karve]

Kevin Buzzard said:

What's the story with the sorrys in tarski.lean -- are they also axioms or should they be fillable?

They should be fillable. The story there is that we just found easier access to proofs in the Euclid and Hilbert system and hence we prioritized those over Tarski's. We have all of Tarski's axioms in place but it's a very rough draft since we haven't really used them to prove any results.

[Kevin Buzzard]

Another interesting thing to do would be to show that the affine spaces which have just appeared in mathlib were a model for these axioms

[Heather Macbeth]

And to show that the disk model of the hyperbolic plane is a model for a non-parallel-postulate variant! IIRC this is on the Freek list.

[Kevin Buzzard]

Aiming for a sorry-ftee Freek statement would be brilliant. Freek is specifically agnostic about the precise form of the statement you prove, he told me he did this intentionally; anything that can be interpreted as a formalisation of the heart of the problem will do. You might be able to turn this into a little piece for the Exp Math special issue, the deadline is December

[Vaibhav Karve]

Whoa! These are great ideas. I will need to look more closely at what these models entail, but thanks a lot for the suggestions.