Nicolò Cavalleri (Jul 26 2021 at 10:21): 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!
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.
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.
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: Sep 23 2023 at 14:01 UTC