Stream: Is there code for X?
Kevin Buzzard (Apr 13 2020 at 22:19):
Can we prove
I'm sorry to use this stream for these questions. I haven't been keeping up with analysis at all and it's been moving fast. I am just looking at what our undergraduates do in their methods course and am wondering how much of it we can currently formalise.
Kevin Buzzard (Apr 13 2020 at 23:00):
PS I am not sure that I care which theory of integration one uses here, I am just looking for something which looks to a mathematician like it might say one of the theorems above.
Patrick Massot (Apr 14 2020 at 07:52):
No, there is a stuck PR that would allow to do that, but the author disappeared.
Yury G. Kudryashov (Apr 14 2020 at 17:38):
I can take over this PR once I'm done grading the exam.
Yury G. Kudryashov (Apr 14 2020 at 19:09):
If @Jeremy Avigad will say that it's OK.
Yury G. Kudryashov (Apr 14 2020 at 19:10):
Jeremy says that a couple of weeks ago @Joe said that he's going to come back to these PRs.
Jeremy Avigad (Apr 14 2020 at 19:18):
Yes, it is o.k. with me. I asked Joe to coordinate, so hopefully he will respond to the ping.
Last updated: May 07 2021 at 19:12 UTC