Zulip Chat Archive

Stream: new members

Topic: Axiomatic projective geometry

Stepan Holub (Oct 06 2022 at 08:22):


Here in Prague we start a new seminar on axiomatization of projective geometry (roughly along axioms by Veblen and Young , 1910 and 1917). I have quite extensive experience with Isabelle but in this seminar we are toying with the idea to formalize the axiomatic system in Lean where we are all complete beginners. The ultimate goal is to show that the theory is complete and decidable, but the formalization would be interesting even without that.
Is there anything similar in Lean already? Both in the field of projective geometry, but also in the logical direction of showing any theory to be complete and/or decidable? I am superficially aware of a related work in Coq (GeoCoq), and I also found in the chat that in 2019 there were some plans to work on projective geometry.

Any comment or suggestion will be appreciated.


Anthony Bordg (Oct 06 2022 at 09:30):

@Stepan Holub
If you're familiar with Isabelle but not with Coq, you could have a look at the entry Projective Geometry in the AFP and import it in Lean, possibly with some modifications depending on your goals. This formalisation was itself adapted from a similar formalisation in Coq.

Yaël Dillies (Oct 06 2022 at 09:35):

Let me cc @Bhavik Mehta who has been recently working on getting some of the results of the Coq paper on PG(3, 2) by Magaud (https://dpt-info.di.unistra.fr/~magaud/talk-itp2022-magaud.pdf) without bash.

Bhavik Mehta (Oct 06 2022 at 11:14):

I also converted a lot of GeoCoq into Lean, but mostly focusing on the geometric results rather than logical facts

Ruben Van de Velde (Oct 06 2022 at 11:17):

Better to focus on the illogical facts?

Adam Topaz (Oct 06 2022 at 13:44):

I had a student over the summer develop some projective geometry in mathlib, but focusing only on projective spaces associated to vector spaces over fields, not the axiomatic approach. He has a branch somewhere which gives the necessary tools one needs to prove the axioms of an abstract projective geometry for such projective spaces (among many other things). Our plan was to advance toward the fundamental theorem of projective geometry.

I’ll try to look around and post some links to this stuff later today.

Junyan Xu (Oct 07 2022 at 03:28):

I'm not sure whether these axioms are what you have in mind, because they don't seem to be complete in the normal model theoretic sense docs#first_order.language.Theory.is_complete, because there are finite models of different cardinalities.

Since this is a finite axiomatization, completeness (in the normal sense) trivially implies decidability. Maybe by completeness you mean it only has the intended models, i.e. projective spaces over division rings?

Stepan Holub (Oct 08 2022 at 11:50):

@Anthony Bordg
Anthony, your AFP entry will certainly be useful. Thanks.

Stepan Holub (Oct 08 2022 at 11:58):

@Junyan Xu
Specifically, I meant the theory of real projective plane being complete. (Yes, complete implies decidable here. The stress on decidable is unnecessary but motivated by interest in efficient decision procedures.)

Last updated: Dec 20 2023 at 11:08 UTC