Zulip Chat Archive

Hey! My name is Abdullah Uyu. I am a senior mathematics student at Galatasaray University, Turkey. This year, I am working on my graduation project and I want to work on a not yet formalized theorem. While I was browsing web, I have found this page: https://leanprover-community.github.io/100-missing.html I am particularly interested in Desargue's Theorem in the list. Is this list up to date?

abdullah uyu (Oct 21 2023 at 13:23):

I have also searched the theorem on the library documentation and have not found it in the library. I am asking that is, are those theorems still waiting to be formalized?

Yaël Dillies (Oct 21 2023 at 13:24):

Hey! Welcome. I believe nobody has done Desargues yet, although I shall warn you that formalising geometry is surprisingly deceptive.

Patrick Massot (Oct 21 2023 at 14:10):

Bienvenue Abdullah ! You should coordinate with @Joseph Myers and @André Hernández-Espiet (Rutgers) if you want to work on elementary geometry.

Kevin Buzzard (Oct 21 2023 at 14:26):

Abdullah, if you want to see an example of what a solution to an IMO geometry problem looks like, then you can check out Joseph' work here https://github.com/leanprover-community/mathlib4/blob/master/Archive/Imo/Imo2019Q2.lean . Note that there are many, many steps in the Lean proof of this IMO problem which one would never write on paper because they are "obvious from the picture".

André Hernández-Espiet (Rutgers) (Oct 21 2023 at 18:07):

My work uses Avigad's framework (https://www.andrew.cmu.edu/user/avigad/Papers/formal_system_for_euclids_elements.pdf) in order to prove Book I of Euclid's Elements. You can find the code here: https://github.com/ah1112/synthetic_euclid_4 . It is currently in the process of being PR'ed. Let me know if you have any questions!

Joseph Myers (Oct 21 2023 at 23:52):

Desargues is a projective theorem; it should be proved first for projective spaces (over an arbitrary division ring, not just the reals) and then versions for affine spaces (again, over an arbitrary division ring) can be deduced from that.

abdullah uyu (Oct 22 2023 at 17:24):

Thank you so much for the warm reception. I will read the solution @Kevin Buzzard. I will also take a look at the paper and the code @André Hernández-Espiet (Rutgers). @Joseph Myers : Exactly my chain of thoughts! I was actually going to ask about that.

abdullah uyu (Oct 22 2023 at 17:40):

As I understand, we also don't have projective spaces defined in the library.

abdullah uyu (Oct 22 2023 at 17:41):

But we have division rings!

abdullah uyu (Oct 22 2023 at 17:46):

No, we have projective spaces: https://leanprover-community.github.io/mathlib4_docs/Mathlib/LinearAlgebra/ProjectiveSpace/Basic.html

Kevin Buzzard (Oct 22 2023 at 19:47):

The phrase "projective space" means different things to different people. There are algebraic geometers, combinatorial people and synthetic geometers

abdullah uyu (Nov 08 2023 at 20:40):

@Kevin Buzzard I am slowly learning the distinctions as we are reading the book "Modern Projective Geometry" by Claude-Alain Faure and Alfred Frölicher. The book proves the result through endomorphisms and its framework is hopefully appropriate.

abdullah uyu (Nov 26 2023 at 17:16):

Kevin Buzzard said:

The phrase "projective space" means different things to different people. There are algebraic geometers, combinatorial people and synthetic geometers

So, let me share what I am at, at the moment: The book starts with an axiomatization, and it immediately gives "projectivization of a vector space" as an example. We have also read the declaration of the projectivization in mathlib4, and it seems what we want.

We have covered a basic proposition saying $\mathscr{P}(V \times K) \cong V \coprod \mathscr{P}(V)$ .

Anand Patel (Dec 11 2023 at 17:10):

Dear all,

My name is Anand Patel and I'm a professor (alg. geometry) at Oklahoma State University. For next semester's undergraduate "Intro to Math Research" course I thought I would try with the students to formalize some beginning spatial projective geometry (purely synthetic, as in Baker's Principles of Geometry Volumes).

Problem: I have 0 coding skills.
Question: How do I go about this? My naive dream is: First we settle on some axioms, maybe not the best or most general, but just something to get us going. Then we try to build to, say, Desargues theorem.

Appreciate any help!

Kevin Buzzard (Dec 11 2023 at 17:59):

You show the students some good references (e.g. Mathematics In Lean) and then you just rely on some of them getting really good and helping the others. Ask here to get the main definitions right. If they're maths undergrads (sounds like they are) then I can send you a link to the Xena Discord, which is full of maths undergraduates asking questions and learning.

Anand Patel (Dec 11 2023 at 18:15):