Zulip Chat Archive
Stream: Is there code for X?
Topic: Exterior Differential Systems
Colleen Robles (Jul 09 2022 at 10:20):
Hi, I'm new to both Lean and Tulip. I just watched Kevin Buzzard's great ICM talk, and am wondering: does the library contain any materials on Exterior Differential Systems?
Kevin Buzzard (Jul 09 2022 at 10:27):
From nLab: "The existing literature on exterior differential systems is actually a bit unclear about which additional assumptions on J are supposed to be a crucial part of the definition. " :-) Humans had better make sure they know a definition before computers have a chance to understand it! But I think the answer to your question is "no" -- we have manifolds but very little more, we are still working on de Rham cohomology and differentials, for example. These things are do-able, it's just a case of people doing it.
Colleen Robles (Jul 09 2022 at 10:58):
@Kevin Buzzard
Kevin Buzzard said:
From nLab: "The existing literature on exterior differential systems is actually a bit unclear about which additional assumptions on J are supposed to be a crucial part of the definition. " :-) Humans had better make sure they know a definition before computers have a chance to understand it! But I think the answer to your question is "no" -- we have manifolds but very little more, we are still working on de Rham cohomology and differentials, for example. These things are do-able, it's just a case of people doing it.
Many thanks. I'm interested in learning more. Do you know of anyone at Duke U (or in North Carolina) with experience with one of these formal theorem proving systems?
Patrick Massot (Jul 09 2022 at 11:12):
I don't think we have anyone from Duke yet. You are very welcome to become the first one!
Patrick Massot (Jul 09 2022 at 11:14):
It's funny because when I read your first message mentioning exterior differential systems I thought it would be nice to have Bryant joining us since he is already very active on mathoverflow. I guess EDS theory is very active at Duke.
Johan Commelin (Jul 09 2022 at 11:24):
@Colleen Robles I know some people in Freiburg (-; How long will you be around?
Colleen Robles (Jul 09 2022 at 12:16):
@Johan Commelin Thanks for your message. Yes, it would be great to talk. I'm in Freiburg until the end of July.
Johan Commelin (Jul 09 2022 at 12:18):
I'm in the US the upcoming week. So there should be two weeks left after that.
Last updated: Dec 20 2023 at 11:08 UTC