Zulip Chat Archive

Stream: maths

Topic: computable functions of reals


view this post on Zulip Johan Commelin (Nov 30 2018 at 14:25):

In my "ordinary maths" research I was confronted with the paper "Computable functions of reals" by Tent and Ziegler, which is really funny because:

I'dd like to hear whether others think that these lower-elementary and elementary functions are close to be Leanable or not.

view this post on Zulip Patrick Massot (Nov 30 2018 at 14:40):

Noooooooooo!

view this post on Zulip Johan Commelin (Nov 30 2018 at 14:40):

Did I say something wrong?

view this post on Zulip Patrick Massot (Nov 30 2018 at 14:40):

Johan, please delete that thread before Mario sees it!

view this post on Zulip Johan Commelin (Nov 30 2018 at 14:41):

@Mario Carneiro Did you see this thread already, or can I still delete it?

view this post on Zulip Patrick Massot (Nov 30 2018 at 14:41):

Remember we still need to be able to handle modules over several base rings

view this post on Zulip Patrick Massot (Nov 30 2018 at 14:42):

Now is not a good time to tempt Mario with computability questions

view this post on Zulip Johan Commelin (Nov 30 2018 at 14:42):

Right, and there are like 8 PRs on category theory waiting to be merged...

view this post on Zulip Patrick Massot (Nov 30 2018 at 14:42):

That too

view this post on Zulip Patrick Massot (Nov 30 2018 at 14:42):

Except you, Reid and Scott keep changing everything, and even you don't understand anymore what PR depends on what, and what PR is obsolete

view this post on Zulip Patrick Massot (Nov 30 2018 at 14:43):

So I guess Mario and Johannes wisely wait for dust to settle

view this post on Zulip Kenny Lau (Nov 30 2018 at 16:14):

what about my 2 PR about ring theory


Last updated: May 12 2021 at 07:17 UTC