Stream: maths

Topic: computable functions of reals

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.

Noooooooooo!

Johan Commelin (Nov 30 2018 at 14:40):

Did I say something wrong?

Johan Commelin (Nov 30 2018 at 14:41):

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

Patrick Massot (Nov 30 2018 at 14:41):

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

Patrick Massot (Nov 30 2018 at 14:42):

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

Johan Commelin (Nov 30 2018 at 14:42):

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

That too

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

Patrick Massot (Nov 30 2018 at 14:43):

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