tarski axiom geometry

Stream: maths

[Tchsurvives]

https://github.com/ImperialCollegeLondon/xena-UROP-2018/tree/master/src/Geometry i found this (for the imo grand challenge project)

[Tchsurvives]

but it seems like i am having problem importing geometry.axioms in tarski_1.lean

[Tchsurvives]

first it takes a long time to load (lean just says Loading...) and after a long time it says invalid import: algebra.ring invalid object declaration, environment already has an object named 'units._inst_1'

[Tchsurvives]

anyone had any success getting the project up and running? i am keen to try my hand at the xena project

[Kevin Buzzard]

This is a very very old repo

[Kevin Buzzard]

I had a student do a much better job this summer

[Kevin Buzzard]

I'm not at a computer right now unfortunately

[Kevin Buzzard]

https://ja1941.github.io/hilberts-axioms/

[Kevin Buzzard]

https://github.com/Ja1941/hilberts-axioms

contains information about how to install the project and prove some theorems in Euclid's Elements using it.

i am keen to try my hand at the xena project

The Xena Project is an attempt to get mathematicians engaging with the theorem prover community, so if you're posting here already then my work is done.

[Tchsurvives]

i see, thanks! ill check that link out @Kevin Buzzard

[Bhavik Mehta]

In the GeoLean branch of mathlib I also did a development of Tarskis axioms, covering about 70% of the Tarski work in the GeoCoq project

[Ruben Van de Velde]

Sounds like we should land at least one of those approaches!

[Bhavik Mehta]

I think both would be valuable! The axiom systems are both interesting, and we can keep Joseph's development as the 'intended' case while the axiomatic ones are treated as separate theories

[Tchsurvives]

i have been looking at the ja1941 project @Kevin Buzzard may I ask who i can ask for relevant help? i am trying my hand at understanding the structure and intend to contribute more theorems as part of the imo grand challenge project

[Kevin Buzzard]

The project was written by @Tianchen Zhao

[Tianchen Zhao]

Can you give me some example problems you want to do in the imo project? The repo cannot formalize some complicated geometry problems yet, but this is definitely possible by adding more components to it. I
Tchsurvives said:

i have been looking at the ja1941 project Kevin Buzzard may I ask who i can ask for relevant help? i am trying my hand at understanding the structure and intend to contribute more theorems as part of the imo grand challenge project

have a webpage explaining some difficult theorems in the repo and in the end there is also a list of things to add. You can check them here https://ja1941.github.io/hilberts-axioms/ and feel free to ask me if you have any questions.

[Tchsurvives]

@Tianchen Zhao hi there! awesome project :) i tried to write a proof of the midpoint theorem as an exercise, but i had difficulty formalising what it means for two lines to be parallel. i wasn't sure if that was due to my inaptitude or because it wasnt written yet.

[Tchsurvives]

i would love to study and contribute, thanks for your help!

[Tianchen Zhao]

Tchsurvives said:

Tianchen Zhao hi there! awesome project :) i tried to write a proof of the midpoint theorem as an exercise, but i had difficulty formalising what it means for two lines to be parallel. i wasn't sure if that was due to my inaptitude or because it wasnt written yet.

Thank you! It's so happy to see people want to contribute to this project. Now it's not provable yet, but we just need one more step to prove it. I did update something on parallelism but I forget to push to github. I just pushed them now and you can have a look. Parallelism is simply defined by two lines without intersections. I am now proving corresponding angles for parallel lines are equal. It's a result by contradiction and that exterior angles are larger than the interior. With this lemma we will be ready to prove the midpoint theorem.

[Tianchen Zhao]

Tchsurvives said:

Tianchen Zhao hi there! awesome project :) i tried to write a proof of the midpoint theorem as an exercise, but i had difficulty formalising what it means for two lines to be parallel. i wasn't sure if that was due to my inaptitude or because it wasnt written yet.

We are now ready to prove midpoint theorem. I just drafted the proof that corresponding or alternative angles are equal iff parallel. It's mostly done with some sorry which is not hard to fill. I will complete them later (but feel free to try them in as exercises too).

[Tchsurvives]

great! :D ill take a look at it

[Tchsurvives]

it seems like we have timezone differences, i stay in Singapore, what's your timezone?

[Johan Commelin]

You can view someones user profile to see their local time. Of course there is no guarantee that it's correct, but it usually is.

[Tchsurvives]

haha either he works at 4am or his local time is off

[Kevin Buzzard]

He's a student in London

[Tchsurvives]

Screenshot-2021-10-23-at-4.29.53-PM.png

[Tchsurvives]

it seems like this symbol isnt defined? (edit: it works now)

[Scott Morrison]

Please see #mwe and #backticks. It's hard to help when we don't know what you're doing!

[Tchsurvives]

alright sorry! im not sure why not it works now, it seems like i need to open the files in vs code at least once for it to load...

[Tchsurvives]

https://github.com/tch1001/hilberts-axioms/commit/09f0037856a9d524ce19e8d5f2d7ede32d9a0751 I have attempted to try my hand at ang_lt_supplementary, but I think I need a definition of a "flipped ray" (vertically opposite angles are equal, corollary 9.3 in hartshone's book)

[Tchsurvives]

do you think you could define flip_ray for me?

[Tchsurvives]

:)

[Tianchen Zhao]

Tchsurvives said:

alright sorry! im not sure why not it works now, it seems like i need to open the files in vs code at least once for it to load...

I just filled all the blanks in corresponding angles and alternative angles. For some hints, you might need the following to prove midpoint theorem:

1. extend_congr_seg'
   2. SAS
   3. alternative_eq_iff_parallel
   4. ASA
      Remind me if you finish the proof or have any questions.

[Tianchen Zhao]

Tchsurvives said:

https://github.com/tch1001/hilberts-axioms/commit/09f0037856a9d524ce19e8d5f2d7ede32d9a0751 I have attempted to try my hand at ang_lt_supplementary, but I think I need a definition of a "flipped ray" (vertically opposite angles are equal, corollary 9.3 in hartshone's book)

I already proved vertical angles are congruent in congruence/baisc.lean, although without explicitly defining flipped ray.

[Kei TSUKAMOTO]

Hi! I’m Kei Tsukamoto. I’d like to join the project about formalizing tarski’s axiom geometry using Lean with my friend Shun . Could anyone tell us how the project is going and what we should do now?

[Yaël Dillies]

cc @Bhavik Mehta

[Bhavik Mehta]

I'm not really sure there's an active project at the moment - the only formalisation of Tarski's axioms in Lean I know of is my GeoLean project, but that was designed more as a direct port of the Coq version rather than a Lean-style development

[Kevin Buzzard]

I have had several Imperial students doing projects formalising geometry axiomatically e.g. here, and they all made standalone projects rather than trying to get stuff into mathlib. For me, any new formalisation should attempt to get to the "next level" which would be using widgets to generate diagrams, which would mean doing a formalisation in Lean 4.

[Joseph Myers]

I'd suggest aiming for Freek's item 12, The Independence of the Parallel Postulate, by proving a complete characterization of instances of versions of axiomatic geometry with and without the parallel postulate (showing that the instances of the former are exactly Euclidean spaces of appropriate dimension, and instances of the latter are exactly Euclidean and hyperbolic spaces of appropriate dimension) - setting things up in appropriate generality to be able to handle spaces of different dimension and to be able to handle the hyperbolic case, and aiming to get things into geometry.tarski in mathlib (with room for also having e.g. geometry.hilbert or geometry.avigad for other sets of axioms).

[Shun Nakatani]

Joseph Myers said:

I'd suggest aiming for Freek's item 12, The Independence of the Parallel Postulate, by proving a complete characterization of instances of versions of axiomatic geometry with and without the parallel postulate (showing that the instances of the former are exactly Euclidean spaces of appropriate dimension, and instances of the latter are exactly Euclidean and hyperbolic spaces of appropriate dimension) - setting things up in appropriate generality to be able to handle spaces of different dimension and to be able to handle the hyperbolic case, and aiming to get things into geometry.tarski in mathlib (with room for also having e.g. geometry.hilbert or geometry.avigad for other sets of axioms).

Can you explain what “Freek’s item 12” refers to?

[Mauricio Collares]

https://www.cs.ru.nl/~freek/100/

[Shun Nakatani]

Bhavik Mehta said:

I'm not really sure there's an active project at the moment - the only formalisation of Tarski's axioms in Lean I know of is my GeoLean project, but that was designed more as a direct port of the Coq version rather than a Lean-style development

Your GeoLean project is impressive!
But what change would make it more lean-style?

[Julien Narboux]

What is the current state of axiomatic geometry in Lean ? I think porting GeoCoq should not be too hard (Roland Coghetto has already ported a large part of GeoCoq to Isabelle). In GeoCoq we have the formalization of axioms systems of Tarski, Hilbert, Euclid, and links between them. We have the fact that one can reconstruct a field in the Euclidean case (arithmetization of geometry). I am open to co-advise an internship if someone is interested.

[Kevin Buzzard]

If we can have diagrams as well then I would love to take this into schools in the UK and show the 16 year olds how the Euclidean geometry they learn can be formalised, and how much work it is to make it rigorous. So for me a great goal would be the "circle theorems" (of which there are about 6, e.g. angle at centre equals twice angle at circumference etc). But I don't know anything about how to make diagrams (widgets) in Lean.

[Patrick Massot]

Many students worked on that, but it was never polished enough to become part of mathlib. I agree that porting GeoCoq should be the way to go.

[Wen Yang]

Some people are working on Euclidean Geometry: https://github.com/jjdishere/EG

[Alex Kontorovich]

I think there's going to be an announcement quite soon from @André Hernández-Espiet (Rutgers) about formalizing @Jeremy Avigad's axioms and using them to "naturally" formalize Euclid's Book 1... https://github.com/ah1112/synthetic_euclid_4

[Newell Jensen]

What would be nice is, once the foundations are laid in these projects is to get that into mathlib so that others can contribute to the formalization of Euclid's Elements so it can be more of a community effort instead of groups working disparately.

[Kevin Buzzard]

The biiiiig problem with this is that there are many competing axiomatic formalisations of geometry

[Kevin Buzzard]

The advantage of Julian's approach is that he did all of them :-)

[Newell Jensen]

Yes, agreed, all of them and links between them are even better. I was referring to Alex and Wen's project mentions.

[Kevin Buzzard]

Earlier in the thread I cite two more formalisations which came out of Imperial when were experimenting back in the early days.

[Newell Jensen]

@Julien Narboux what would be the first steps for starting the port?

[Kevin Buzzard]

Julien's suggestion was: "find a good student" :-)

[Alex Kontorovich]

Newell Jensen said:

What would be nice is, once the foundations are laid in these projects is to get that into mathlib so that others can contribute to the formalization of Euclid's Elements so it can be more of a community effort instead of groups working disparately.

Yes, your point is very well taken...

[Yaël Dillies]

Kevin Buzzard said:

The biiiiig problem with this is that there are many competing axiomatic formalisations of geometry

The response to that is to have them all in the form of typeclasses and implications between them.

[Bhavik Mehta]

Julien Narboux said:

What is the current state of axiomatic geometry in Lean ? I think porting GeoCoq should not be too hard (Roland Coghetto has already ported a large part of GeoCoq to Isabelle). In GeoCoq we have the formalization of axioms systems of Tarski, Hilbert, Euclid, and links between them. We have the fact that one can reconstruct a field in the Euclidean case (arithmetization of geometry). I am open to co-advise an internship if someone is interested.

I have a port of a large portion of GeoCoq in Lean, in the GeoLean branch of mathlib3

[Bhavik Mehta]

The main issue with it is that the Coq style doesn't work well with the mathlib style - GeoCoq alone had some theorems duplicated with different names inside itself, so there's some work to tidy it up, and then further work to set up the theory to be good lean quality.

[Patrick Massot]

Did you open a GeoCoq issue about those duplicated theorems?

[Bhavik Mehta]

I didn't - my impression was that that project was finished and so issues wouldn't be particularly useful

[André Hernández-Espiet (Rutgers)]

I am ready to PR this, can I please have GitHub access for Lean 4? My GitHub user is ah1112

[Riccardo Brasca]

You should have an invitation.

[André Hernández-Espiet (Rutgers)]

This is now PR #7300. It's giving me a build error I do not understand. It compiles perfectly on my local machine. Any help would be much appreciated.

[Alex J. Best]

One error is that you haven't added the new files you added to the file Mathlib.lean which is a sort of directory of all files within mathlib

[Alex J. Best]

And I can reproduce the second error locally, there is presumably some issue with the tactics youve written that appears in quad_add_of_quad

[Alex J. Best]

its easy to miss such issues as the only show up as a pop-up in vscode but there is some array index out of bounds in your tactic

[Alex J. Best]

In this case you can fix the immediate issue by changing the last line of that proof to

    (not_online_of_sameside (by perma[feL] :))]

perhaps the issue is something to do with tactics being handed goals with metavariables in

[Alex J. Best]

it looks like the same issue comes up later in the file also so at the very least it would be better to change the tactic to print good error messages in this case

[Alex J. Best]

Feel free to say here if you want more info on how to debug / fix this, happy to help

[Alex Kontorovich]

Tagging @Vladimír Sedláček who wrote the tactics; hopefully between Vlada and Andre (and Alex's gracious help), this can be fixed...

[André Hernández-Espiet (Rutgers)]

Ok, I added the files toMathlib.lean, so it is not complaining about that anymore. I will talk with @Vladimír Sedláček and if we can't figure it out, then we'll ask for help. Thanks a lot!

[Joseph Myers]

Since there are many different axiom systems, I think you should put this in Mathlib.Geometry.Avigad not Mathlib.Geometry.Synthetic (leaving room for future addition of Mathlib.Geometry.Tarski and Mathlib.Geometry.Hilbert and proofs of how the different axiom systems are related). The module doc string definitely needs to give a reference to the source of the particular set of axioms being used.

[André Hernández-Espiet (Rutgers)]

Joseph Myers said:

Since there are many different axiom systems, I think you should put this in Mathlib.Geometry.Avigad not Mathlib.Geometry.Synthetic (leaving room for future addition of Mathlib.Geometry.Tarski and Mathlib.Geometry.Hilbert and proofs of how the different axiom systems are related). The module doc string definitely needs to give a reference to the source of the particular set of axioms being used.

Ok! I modified the directories to reflect this. Let me know if you think I should do anything else.

[Vláďa Sedláček]

Alex J. Best said:

In this case you can fix the immediate issue by changing the last line of that proof to

    (not_online_of_sameside (by perma[feL] :))]

perhaps the issue is something to do with tactics being handed goals with metavariables in

Indeed, it seems that the metavariables are the issue - the index out of bounds error does not happen when the argument type is made explicit. Is that what your : fix does?

I believe the underlying culprit is the last line of the following MWE, which internally calls Array.get! inside getNthArgName. Any ideas how to fix this?

import Lean

universe u1 u2 u3
class incidence_geometry :=
(point : Type u1)
(line : Type u2)
(sameside : point → point → line → Prop)
(sameside_symm : ∀ {a b : point}, ∀ {L : line}, sameside a b L → sameside b a L)

variable [i : incidence_geometry]
open incidence_geometry

namespace Lean.Elab.Tactic

def getFVars (e : Expr) : Array FVarId :=
  (Lean.collectFVars {} e).fvarIds

def getNthArgName (tgt : Expr) (n : Nat) : MetaM Name :=
  ((getFVars (Lean.Expr.getArg! tgt n)).get! 0).getUserName

elab "sameside_nf" : conv => withMainContext do
  let tgt ← instantiateMVars (← Conv.getLhs)
  let n1 ← getNthArgName tgt 1
  let n2 ← getNthArgName tgt 2
  if n2.lt n1 then
    evalTactic (← `(tactic| rw [@sameside_symm _ _] ))

syntax "perm" ("at " ident)? : tactic
macro_rules
  | `(tactic| perm at $name) =>`(tactic|
    (try conv at $name in (occs := *) length _ _ => all_goals sameside_nf))

open Lean Meta in
def haveExpr (n : Name) (h : Expr) :=
  withMainContext do
    let t ← inferType h
    liftMetaTactic fun mvarId => do
      let mvarIdNew ← Lean.MVarId.assert mvarId n t h
      let (_, mvarIdNew) ← Lean.MVarId.intro1P mvarIdNew
      return [mvarIdNew]

open Parser Tactic Syntax

syntax "havePerms" (" [" term,* "]")? : tactic
elab_rules : tactic
  | `(tactic| havePerms $[[$args,*]]?) => withMainContext do
    let hyps := (← ((args.map (TSepArray.getElems)).getD {}).mapM (elabTerm ·.raw none)).toList
    for h in hyps do
      haveExpr "this" h
      evalTactic (← `(tactic| perm at $(mkIdent "this")))

[Alex J. Best]

The : essentially delays the elaboration of that tactic, which I think in this case causes lean to fill in the mvars by the time your tactic gets called.

[Alex J. Best]

Seeing as your normalization strategy really relies on having the user names available

[Alex J. Best]

I think the best fix is probably just to catch and throw an error in your tactics whenever the goal has some unassigned mvars in

[Alex J. Best]

And let the user be more specific about where the problem is

[Alex J. Best]

So maybe instead of ((getFVars (Lean.Expr.getArg! tgt n)).get! 0).getUserName in getNthArgName you could use (untested)

do
  let some id := Lean.Expr.fvarId? (Lean.Expr.getArg! tgt n) | throwError "argument {n} is not a free variable"
  id.getUserName

[Vláďa Sedláček]

Thanks a lot! With your suggested change, only two proofs seem to be broken now, and hopefully the delayed elaboration and/or some slight refactoring will take care of that.

[André Hernández-Espiet (Rutgers)]

I have two linter issues that I don´t really understand, if one of you could help me.
One of them is saying I have bad universe levels. How do I fix this?
The other one says to Remove matcher: gcc. How do I solve this?

[Scott Morrison]

@André Hernández-Espiet (Rutgers), can you post a link to a CI run or otherwise a branch?

[André Hernández-Espiet (Rutgers)]

Sorry, I am kind of new to this. What is a CI run? The branch info is in PR #7300 perhaps?

[Scott Morrison]

That's great, thanks. (By "a CI run" I meant this link: https://github.com/leanprover-community/mathlib4/actions/runs/6280035987/job/17056653298?pr=7300)

[Alex J. Best]

The remove matcher isn't a failure. So you only need to solve the universes thing

[Scott Morrison]

The "remove matcher" you should ignore --- and we should get rid of.

[Alex J. Best]

Scott Morrison said:

The "remove matcher" you should ignore --- and we should get rid of.

Its a logging message from an action we use so i'm not sure we can get rid of it completely

[André Hernández-Espiet (Rutgers)]

Scott Morrison said:

That's great, thanks. (By "a CI run" I meant this link: https://github.com/leanprover-community/mathlib4/actions/runs/6280035987/job/17056653298?pr=7300)

Oooh that's good to know.

[Scott Morrison]

Alex J. Best said:

Scott Morrison said:

The "remove matcher" you should ignore --- and we should get rid of.

Its a logging message from an action we use so i'm not sure we can get rid of it completely

Worth a try: https://github.com/liskin/gh-problem-matcher-wrap/issues/15

[Alex J. Best]

As for the universes thing, it seems unlikely to me that you'd need to have points, lines, circles in different universes for any reason later, so you could make them all the same. And maybe the linter is a hint that things could be annoying later with so much flexibility

[André Hernández-Espiet (Rutgers)]

Ok, I will do that and see if it builds. I can try #lint to check locally, right?

[André Hernández-Espiet (Rutgers)]

It worked!

[Scott Morrison]

#7346 will silence the confusing "remove matcher" message! (Yay this modern github world.)

[Alex Kontorovich]

Andre, it looks like there's a merge conflict. If I understand correctly, this should be cleared with git merge origin/master...

[Julien Narboux]

This is exactly what we do in GeoCoq.

Yaël Dillies said:

Kevin Buzzard said:

The biiiiig problem with this is that there are many competing axiomatic formalisations of geometry

The response to that is to have them all in the form of typeclasses and implications between them.

[Julien Narboux]

Bhavik Mehta said:

The main issue with it is that the Coq style doesn't work well with the mathlib style - GeoCoq alone had some theorems duplicated with different names inside itself, so there's some work to tidy it up, and then further work to set up the theory to be good lean quality.

Yes indeed GeoCoq needs to be cleaned up (there some duplicated lemmas (some are just symmetric of others etc), and some good naming convention should be adopted. Currently it is a mix of names coming from the book of Tarski and our own names.

[Julien Narboux]

No it is not finished, there plenty of extension needed. For example, we are missing trigonometry, areas, etc...

[Julien Narboux]

Newell Jensen said:

Julien Narboux what would be the first steps for starting the port?

I think the main axiom system could be Tarski's, the book by Schwabhauser, Tarski and Szmiliew is very formal and quite easy to follow, and it brings the very important result that one can reconstruct a field. From this, one can derive Hilbert's geometry and the proofs that the two are equivalent. It should not be too difficult based on the existing formalizations that will tell you about all the details and help in case one is stuck on a proof. I guess it is not difficult to port the proofs from Coq to Lean, the first step would be to write the tactics, you need some tactics to deal with pseudo-transitivity of collinearity and symmetries of geometric predicates, etc (see https://adg2023.matf.bg.ac.rs/downloads/slides/IntroductionBoutryNarboux.pdf for a list of tactics). Then each lemma can be reproduced one by one. A difficulty could be that in some chapters at the end, we rely on a tactic based on Gröbner's basis (nsatz in Coq), I don't know if there is an equivalent in Lean4. The proof could be done manually but that would be boring.
Another difficulty is cleaning up: detecting duplicates, giving good names etc.
Sometimes it may well be the case that a long proof can be replaced by a much a simpler one.
Roland Coghetto ported GeoCoq to Isabelle using Sledgehammer, without trying to understand the proofs, I don't know if there is a hammer for Isabelle, that could be an option. The hammer could help also detecting duplicates, and shorter proofs.
Maybe the porting of GeoCoq could be a good opportunity to translate proof from tactic style to a more declarative style, maybe based on tactics like @Patrick Massot 's Lean-Verbose.

Yoan Geran has exported our formalization of Euclid/Book 1 (238 lemmas, 20klocs,15% of
GeoCoq) to Dedukti, and he can translate the proofs back to Coq, HOL-Light, Lean, Matita, PVS and Open Theory.
But the (compressed) size of the translated proofs are multiplied by 10 (Lean, Matita, Coq), 25 (Hol-Light) and 50 (PVS).
So it may not be usable in practice, even if there is room for improvements.
The difficulty is that Dedukti works with lambda terms, and it would be hard to get back some tactics that make the proofs shorter.
For example, in GeoCoq we have a tactic that derive automatically a lot of ndg conditions, for example if A is different from B, then the midpoint of AB is different from A and from B, etc... it applies several rules like that in a forward chaining manner and it completes the context with many NDGs. Maybe some of these NDGs are not actually used in the proof, but it is convenient to have them for automation. If one translates the proofs from the lambda term, one can detect that some part are derived but not used (dead code). So the translation in some sense simplifies the proofs, but in practice because all theses facts are produced by a single call to a tactic, the " simplified " proof is much longer than the original.

[Julien Narboux]

Kevin Buzzard said:

If we can have diagrams as well then I would love to take this into schools in the UK and show the 16 year olds how the Euclidean geometry they learn can be formalised, and how much work it is to make it rigorous. So for me a great goal would be the "circle theorems" (of which there are about 6, e.g. angle at centre equals twice angle at circumference etc). But I don't know anything about how to make diagrams (widgets) in Lean.

Filip Maric has a javascript library to draw sketches. Maybe this can be used in a widget.

[Bhavik Mehta]

Julien Narboux said:

Newell Jensen said:

Julien Narboux what would be the first steps for starting the port?

I guess it is not difficult to port the proofs from Coq to Lean, the first step would be to write the tactics, you need some tactics to deal with pseudo-transitivity of collinearity and symmetries of geometric predicates, etc (see https://adg2023.matf.bg.ac.rs/downloads/slides/IntroductionBoutryNarboux.pdf for a list of tactics). Then each lemma can be reproduced one by one. A difficulty could be that in some chapters at the end, we rely on a tactic based on Gröbner's basis (nsatz in Coq), I don't know if there is an equivalent in Lean4. The proof could be done manually but that would be boring.
Another difficulty is cleaning up: detecting duplicates, giving good names etc.
Sometimes it may well be the case that a long proof can be replaced by a much a simpler one.

For example, in GeoCoq we have a tactic that derive automatically a lot of ndg conditions, for example if A is different from B, then the midpoint of AB is different from A and from B, etc... it applies several rules like that in a forward chaining manner and it completes the context with many NDGs. Maybe some of these NDGs are not actually used in the proof, but it is convenient to have them for automation.

I agree with all of this - in my port of GeoCoq to Lean I did do most of these tactic steps automatically, and used automation to make some of the easy parts even easier. Although the size of the translated proofs was overall shorter than the Coq versions, for me.

[Patrick Massot]

Julien Narboux said:

Kevin Buzzard said:

If we can have diagrams as well then I would love to take this into schools in the UK and show the 16 year olds how the Euclidean geometry they learn can be formalised, and how much work it is to make it rigorous. So for me a great goal would be the "circle theorems" (of which there are about 6, e.g. angle at centre equals twice angle at circumference etc). But I don't know anything about how to make diagrams (widgets) in Lean.

Filip Maric has a javascript library to draw sketches. Maybe this can be used in a widget.

Do you have any link to share?

[Junyan Xu]

The response to that is to have them all in the form of typeclasses and implications between them.

I wonder if we can put a [EuclidWithoutFifthPostulate] instance on upper half plane, unit disk (Poincare or Klein), and E^2 (or any inner product space of dimension 2) and have all theorems apply to them ... Looks like a lot of duplication to be saved. By the way, is there anything about higher dimensional (3D?) geometry, even just writing down the axioms? (Edit: GeoCoq apparently has it, see slide 15.)

[Bhavik Mehta]

Junyan Xu said:

The response to that is to have them all in the form of typeclasses and implications between them.

I wonder if we can put a [EuclidWithoutFifthPostulate] instance on upper half plane, unit disk (Poincare or Klein), and E^2 (or any inner product space of dimension 2) and have all theorems apply to them ... Looks like a lot of duplication to be saved. By the way, is there anything about higher dimensional (3D?) geometry, even just writing down the axioms? (Edit: GeoCoq apparently has it, see slide 15.)

Yeah - you can take a subset of the Tarski axioms and work on >=2D geometry or <=2D geometry, or modify them and fix which dimension you want to work in

[Vláďa Sedláček]

Kevin Buzzard said:

If we can have diagrams as well then I would love to take this into schools in the UK and show the 16 year olds how the Euclidean geometry they learn can be formalised, and how much work it is to make it rigorous. So for me a great goal would be the "circle theorems" (of which there are about 6, e.g. angle at centre equals twice angle at circumference etc). But I don't know anything about how to make diagrams (widgets) in Lean.

I made a small widget demo for visualizing points and lines here: https://github.com/EdAyers/ProofWidgets4/blob/main/ProofWidgets/Demos/Euclidean.lean. I can try extending it for circles as well in the near future.

[Kevin Buzzard]

Another benchmark for formalisation could be Zeilberger's cute geometry textbook https://sites.math.rutgers.edu/~zeilberg/PG/gt.html .

[Vláďa Sedláček]

Here's my attempt, I'll be glad for feedback.
circle_demo1.png
circle_demo2.png
After shift-clicking a subset of hypotheses, they get rendered by Penrose according to your styling rules.
(Before PRing this to ProofWidgets, maybe it makes sense to wait until André's PR #7300 is merged, so that all the geometry can be imported instead of duplicated?)

[Alex Kontorovich]

This is great, Vlada! You can PR yours on top of Andre's and mark it is as dependent on his

[Trebor Huang]

Perhaps the colors should be changed a little bit? At least you can add a css filter that sort of subtracts colors so it's visible in both light and dark mode

[Patrick Massot]

This is fantastic! Could you show us an example involving an actual geometry theorem? You could start with stating that lines from the vertices of a triangle to the middle of the opposite edge share a common point. And then do Feuerbach' s theorem for extra credit.

[Kevin Buzzard]

Or a standard UK high school circle theorem that every 15 year old in my country has to learn, like angle at centre equals twice angle at circumference.

[Vláďa Sedláček]

Thanks for the suggestions! Seeing the reactions, I might reconsider the PR after polishing this a little.
@Trebor Huang We looked into this with @Rohan Karamel today and the colors should now automatically match the VSCode theme. Next level could be adding an infoview panel where you can customize the colors on the fly.
@Patrick Massot @Kevin Buzzard Let's see what I can do. Angles might be slightly tricky to visualize with this setup.
Also @Alex Kontorovich proposed that to improve usability, it would be nice to have the picture drawn automatically with all the hypotheses selected (currently, you have to add them one by one, and the picture is only shown if the cursor is on the line with the corresponding tactic). I'll look into this, but any ideas would be appreciated - perhaps @Wojciech Nawrocki or @Edward Ayers might know?

[Wojciech Nawrocki]

Before PRing this to ProofWidgets, maybe it makes sense to wait until André's PR #7300 is merged, so that all the geometry can be imported instead of duplicated?

Perhaps I am misunderstanding, but you cannot import Mathlib from ProofWidgets because Mathlib depends on ProofWidgets. What you can do, though, is put the visualization code under Mathlib.Tactic.Widget.

[Wojciech Nawrocki]

the colors should now automatically match the VSCode theme

Were you able to use the foreground/tooltipBackground etc constants?

[Wojciech Nawrocki]

to improve usability, it would be nice to have the picture drawn automatically with all the hypotheses selected (currently, you have to add them one by one, and the picture is only shown if the cursor is on the line with the corresponding tactic)

You can change your JS in EuclideanDisplayPanel to ignore props.selectedLocations (ignore the selection) and instead send all the hypotheses to your server_rpc_method for processing. Actually, all the hypotheses are already "there" in the MetaM state introduced by ps.mvar.withContext, so you can just ignore locs and grab all the hypotheses instead.

[Julien Narboux]

Junyan Xu said:

The response to that is to have them all in the form of typeclasses and implications between them.

I wonder if we can put a [EuclidWithoutFifthPostulate] instance on upper half plane, unit disk (Poincare or Klein), and E^2 (or any inner product space of dimension 2) and have all theorems apply to them ... Looks like a lot of duplication to be saved. By the way, is there anything about higher dimensional (3D?) geometry, even just writing down the axioms? (Edit: GeoCoq apparently has it, see slide 15.)

Yes in Tarski's book you already have a lot of results proved without the fifth postulate and in arbitrary dimension. In GeoCoq we have often the assumption that we are at least in 2D.