Stream: Coq users

Topic: Differential geometry


view this post on Zulip Nicolò Cavalleri (Jul 26 2021 at 10:21):

Hi everybody! I am new to Coq (although I have some experience on Lean) and I was wondering what is the current state of Coq with respect to differential geometry. I saw there has been a lot of progress on synthetic differential geometry but I cannot find anything on standard dg!

view this post on Zulip Ben Siraphob (Jul 27 2021 at 16:14):

I too was curious about this so I opened an issue on the Coq topology library about adding manifolds. https://github.com/coq-community/topology/issues/29 Unfortunately I'm not familiar enough with the library or how port (mostly classical) mathematical reasoning into Coq to take on the formalization myself.

view this post on Zulip Stéphane Desarzens (Aug 09 2021 at 05:19):

Its probably easier to do synthetic diff.geo. than to glue together the necessary analysis & topology to do "classical" diff.geo.
But given an easy-to-use library for higher-dimensional derivatives (the contents of an Analysis 2 course), it shouldn't be too difficult. Some linear algebra is of course also necessary.
I don't know (and haven't searched for) compatible libraries for the above.

view this post on Zulip Stéphane Desarzens (Aug 09 2021 at 05:20):

If you have questions about the topology library, just ask me. I might be able to help.


Last updated: Jan 29 2023 at 01:02 UTC