Missing theorems list

Stream: new members

[abdullah uyu]

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]

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]

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

[Patrick Massot]

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

[Kevin Buzzard]

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)]

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]

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]

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]

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

[abdullah uyu]

But we have division rings!

[abdullah uyu]

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

[Kevin Buzzard]

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

[abdullah uyu]

@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]

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]

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]

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]

Kevin Buzzard said:

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.

Thanks for the quick response. Yes, they are mathematics undergraduates. I'd appreciate the link to the Discord!

[Abdullah Uyu]

I have the following snippet where I try to transcribe an axiomatization of a projective geometry: A set $G$ together with a ternary relation $\ell$ satisfying three axioms. In this snippet, $G$ is not visible, and $\ell$ is represented by collinear.

class HasCollinear (P : Type) where
collinear : P → P → P → Prop

export HasCollinear (collinear)

variable {Point : Type} [HasCollinear Point]

axiom l1 (a b : Point) : collinear a b a
axiom l2 (a b p q : Point) : collinear a p q → collinear b p q → p ≠ q →
collinear a b p
axiom l3 (a b c d p: Point) : collinear p a b → collinear p c d →
∃ q : Point , collinear q a c ∧ collinear q b d

On the other hand, there is the projectivization of a vector space in the mathlib4 library. How can I create a projective geometry class of which I can show that the projectivization of a vector space in the library is an instance? Is the following OK?

structure ProjectiveGeometry where
point : Type u
ell : point → point → point → Prop
l1 : ∀ a b , ell a b a
l2 : ∀ a b p q, ell a p q → ell b p q → p ≠ q → ell a b p
l3 : ∀ a b c d p, ell p a b → ell p c d → ∃ q : point , ell q a c ∧ ell q b d

@Kevin Buzzard

[Abdullah Uyu]

Kevin Buzzard said:

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.

Can I join that Discord channel? Could you send me the link? Thank you @Kevin Buzzard

[Abdullah Uyu]

Anand Patel said:

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!

Hello again, how is your journey going? As part of my graduation project, I tried to formalize Desargues's Theorem from the book "Modern Projective Geometry". I couldn't reach to the end but wrote some basic definitions and properties. Here is the repository https://github.com/oneofvalts/desargues