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!

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.

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.

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