I started as a coder in the late 80s. Traded my high-paying IT career for a decade of graduate school near-poverty. Got a maths PhD and climbed the greasy pole to secure a tenure-track job in a maths department. A lifetime of mathing myself and others has been reasonbly fulfilling but now that I am within a stones-throw of retirement I have to contend with the inevitable questions: whas it worth it? Did I follow the right fork in the road? In any case, love the channel and FYI after a lifetime of professing this nonsense I have come to the conclusion that abstract maths is just a branch of software engineering. It's all about organizing, reusing, and documenting "code" in the most efficient and aesthetic way possible. (whatever "efficient" and "aesthetic" mean). I've supervised honours students an a few grad students... some of them exceedingly bright and filled with promise. Like you... Like this channel. I don't say this outloud to them, but all the while I am teaching and supervising my inner thought is "Run... run... run.." Academic mathematics is a vicious racket. We are going to chew you up and spit you out. You are the grist for our mill. Maths is heroin. We are the dealers and you are the junkies. Sure, we use ourselves but at least we get paid well. Chances are you won't get paid well. Might be you won't get paid at all. But you will still need to use. Sorry for sharing. As I said. Love the channel.
Pinning because the reality of post-graduate academia definitely needs more visibility, especially for the talent of the upcoming generations, so that they're well-informed about what they're getting into (though hopefully they won't share my naïvité that got me ignoring all of the warning signs when I dove in). Thanks for your perspective!
My team of experts is working tirelessly on finding a constructive conclusion for whether or not topologists can code. (I'm bouncing some other elegant topological proofs around to see if they drop algorithms)
@@SheafificationOfG looking forward to it. I have a few projects that make sense to look at from a topology view, but I haven't figured out how to program any of the theorems.
@SheafificationOfG what about Homotopy Type Theory? I thought it was like a topologists version of coding, where all the types have a topological relationship? Or is it more of a model producing kind of thing?
I should be noted that while the second proof does not produce an algorithm and shows very clearly that the argument actually only shows that there is a point where f does not not vanish, this does not mean that the first proof is stronger. It shows the same result, and from the view of constructive mathematics, the algorithm produced at 4:19 is not correct in the sense that it doesn’t always hold. This is not just a formality, mind you: If one were to actually implement this algorithm, one would need some procedure to check whether x > 0 or x < 0 or x = 0 (basically: computing the sign function). Such a procedure does not exist, because every computable function on the real numbers is continuous. The problem even has some real-life significance: Suppose we run the algorithm shown in the video on a continuous function [0, 1] \to \R which is extremely small (10^-googol) on the entire interval [1/3, 2/3]. It would be very difficult to tell where the zero is, because each point looks basically like a zero. If you only want an approximate zero, that’s fine, but good look determining whether the actual zero is at 2/5 or at 3/5 (or both).
The function doesn't need to be computed on arbitrary real numbers, though. Assuming that a_0 and b_0 are rational, the algorithm only ever computes f(x) for rational x. That does mean that it can't ever compute the exact value of x_inf if it happens to be irrational (or even in many cases when it's rational). But that limitation was already stated in the video. The algorithm only approximates a solution to an arbitrary degree of precision. But by "approximates a solution" I mean it finds an x arbitrarily close to some exact preimage of 0 - not just an x where f(x) is arbitrarily close to 0. In your example, the algorithm wouldn't give up and say "1/3 looks pretty close but I can't tell whether f(1/3) is really zero or not". Admittedly, the example code given *would* do that, since it assumes that f(x) can be evaluated as a double, and doubles have a fixed maximum precision. But if f is a computable function, then by definition there is some procedure that determines for sure whether f(x) is positive or negative (for a computable input x), and always completes in a finite amount of time. Perhaps a long time, but finite. A binary search algorithm based on this procedure will eventually determine which half of the search interval to continue searching on. And the number of times the interval needs to be halved only depends on how small you want it to be (i.e. how well you want to approximate x), not on the function itself. So you can approximate the true preimage as precisely as needed in a finite amount of time. If the input function is not computable then sure, all bets are off...
@@comexk If f maps rational numbers to rational numbers and it is the case that if the input is given as a/b for integers a and b, then you can compute integers c and d such that the output is c/d, then indeed I think the proof goes through constructively. There are certainly other conditions which guarantee that the algorithm works. However, your I don’t agree with your more general claim that „if f is computable, then there is a procedure that determines whether f(x) is positive or negative (for computable input).“ That depends on what you mean by computable, and how you encode real numbers. Again, if computable means something like in the first paragraph, ok. For instance, x \mapsto x - sqrt(2) is zero iff the input is sqrt(2), so determining whether the function vanishes is equivalent to deciding whether the input is sqrt(2), which is undecidable. (For me, if nothing else is said, real numbers are encoded as infinite sequences of 0 and 1 (and ,) interpreted as binary numbers, and a real function is computable when there is an algorithm that determines the first n digits of the output given a sufficiently large number of input digits.) For the specific application at hand, one does not actually need all computable inputs, but only rational inputs, as you pointed out. Indeed, for any function f whatsoever, there is a procedure which determines for a pair of integers (a, b) whether f(a/b) = 0. This procedure does not computably depend on the input, therefore I think this is not constructively a theorem, even if f is restricted to be computable. I cannot currently give a more formal argument. At any rate, it is true constructively that for every n, there is a c_n such that abs(f(c_n)) < 1/n. But this does not allow you to approximate a root to arbitrary precision, because the c_n might be approximations for different zeros. The problem admittedly only occurs for functions whose zero-set has a limit-point, so there is some hope (even though this observation does not help numericists with the problem I pointed out).
iirc, the incomputability of the sign function in R is the only thing that makes it impossible to use R on a computer ( even if you assume infinite memory ), as it's equivalent to making comparison impossible, and i think comparison always ends up being necessary to implement any mathematical operation ( although i forgot the reason. Even if that's not the case, no comparison means absolutely no algorithms )
could you consider things like "constructive mathematics + a real number comparison oracle" to be able to precisely quantify how the first proof is "more constructive" than the second
Sex(A, B) can denote the category of left exact functors between abelian categories A and B. (What I'm trying to say is, don't choose the math degree.)
damn!! i can’t believe you got me to exclude the middle. i read all of kleene and learned intuitionistic first order arithmetic just to be bamboozled into excluding the middle
I don't know why, but your videos don't get to my subscriptions, maybe youtube needs a critical mass of subscribers. Anyway, you defenetly should continue what you are doing, this is brilliant. I am sure you will find your viewer.
I've heard this concept before where a problem has a solution, but that solution can't ever be found. Does this mean the proofs for existence were of the form: "the problem can't not have a solution" ?
Yeah, non-constructive proofs of existence are essentially just proving the impossibility of non-existence. Not worrying about actually providing an example keeps a lot of options open for an elegant or short proof. For example, it's not a difficult exercise to prove non-constructively that transcendental numbers (numbers that are not solutions to polynomial equations with integer coefficients) exist: you can do it by proving that algebraic numbers are countable, but the set of real numbers is uncountable. This proof demonstrates that, in fact, *most* real numbers are transcendental (i.e., if you randomly sample a real number in [0, 1], you have a 100% chance of drawing a transcendental number). However, the proof is non-constructive; it's really just showing that it's impossible for algebraic numbers to account for all real numbers. On the other hand, it takes considerably more work to prove that a specific number (e.g., pi or e) is transcendental.
Bolzano-Weierstrass overlaps nicely with something I have in the oven, so I might add it in as seasoning! (Pretty sure I replied to this already, but I don't see my own response, so idk if UA-cam is bugging or I'm impatient)
For me... Pure math, not applied math, is the ideal course... Next is computer science if the university doesn't have pure math... Both do hard proofs anyway...
While it is certainly true that every connected open subset of R is an open interval, it's not necessary for the abstract proof of the IVT: I only ever need connectivity of the closed interval [a, b], since that is the choice of domain of the continuous function.
@tobiaswolf7996 I‘d differ from Sheafification and say that yes, this is precisely the argument: (1) An interval is connected, (2) the image of an interval is connected, and (3) connected sets are intervals, therefore (T) the image of an interval is an interval. But note that this observation (3) is essentially the example at 7:42.
I started as a coder in the late 80s. Traded my high-paying IT career for a decade of graduate school near-poverty. Got a maths PhD and climbed the greasy pole to secure a tenure-track job in a maths department. A lifetime of mathing myself and others has been reasonbly fulfilling but now that I am within a stones-throw of retirement I have to contend with the inevitable questions: whas it worth it? Did I follow the right fork in the road? In any case, love the channel and FYI after a lifetime of professing this nonsense I have come to the conclusion that abstract maths is just a branch of software engineering. It's all about organizing, reusing, and documenting "code" in the most efficient and aesthetic way possible. (whatever "efficient" and "aesthetic" mean).
I've supervised honours students an a few grad students... some of them exceedingly bright and filled with promise. Like you... Like this channel. I don't say this outloud to them, but all the while I am teaching and supervising my inner thought is "Run... run... run.." Academic mathematics is a vicious racket. We are going to chew you up and spit you out. You are the grist for our mill. Maths is heroin. We are the dealers and you are the junkies. Sure, we use ourselves but at least we get paid well. Chances are you won't get paid well. Might be you won't get paid at all. But you will still need to use.
Sorry for sharing. As I said. Love the channel.
Pinning because the reality of post-graduate academia definitely needs more visibility, especially for the talent of the upcoming generations, so that they're well-informed about what they're getting into (though hopefully they won't share my naïvité that got me ignoring all of the warning signs when I dove in). Thanks for your perspective!
Dang, I was getting real hyped about some algorithms with topology.
My team of experts is working tirelessly on finding a constructive conclusion for whether or not topologists can code.
(I'm bouncing some other elegant topological proofs around to see if they drop algorithms)
@@SheafificationOfG looking forward to it. I have a few projects that make sense to look at from a topology view, but I haven't figured out how to program any of the theorems.
@SheafificationOfG what about Homotopy Type Theory? I thought it was like a topologists version of coding, where all the types have a topological relationship? Or is it more of a model producing kind of thing?
As a proud LEM assumer, I am going to completely ignore the last part of the video
Your stance on LEM is not wrong.
please pump up more content like this, it's some peak humor
Thanks! Definitely got a few more ideas in the attic.
"Do you even code?"
- Professional Codebuilder
The hulk is green from his extensive git commit history.
I should be noted that while the second proof does not produce an algorithm and shows very clearly that the argument actually only shows that there is a point where f does not not vanish, this does not mean that the first proof is stronger. It shows the same result, and from the view of constructive mathematics, the algorithm produced at 4:19 is not correct in the sense that it doesn’t always hold. This is not just a formality, mind you: If one were to actually implement this algorithm, one would need some procedure to check whether x > 0 or x < 0 or x = 0 (basically: computing the sign function). Such a procedure does not exist, because every computable function on the real numbers is continuous. The problem even has some real-life significance: Suppose we run the algorithm shown in the video on a continuous function [0, 1] \to \R which is extremely small (10^-googol) on the entire interval [1/3, 2/3]. It would be very difficult to tell where the zero is, because each point looks basically like a zero. If you only want an approximate zero, that’s fine, but good look determining whether the actual zero is at 2/5 or at 3/5 (or both).
username checks out
The function doesn't need to be computed on arbitrary real numbers, though. Assuming that a_0 and b_0 are rational, the algorithm only ever computes f(x) for rational x. That does mean that it can't ever compute the exact value of x_inf if it happens to be irrational (or even in many cases when it's rational). But that limitation was already stated in the video. The algorithm only approximates a solution to an arbitrary degree of precision.
But by "approximates a solution" I mean it finds an x arbitrarily close to some exact preimage of 0 - not just an x where f(x) is arbitrarily close to 0. In your example, the algorithm wouldn't give up and say "1/3 looks pretty close but I can't tell whether f(1/3) is really zero or not". Admittedly, the example code given *would* do that, since it assumes that f(x) can be evaluated as a double, and doubles have a fixed maximum precision. But if f is a computable function, then by definition there is some procedure that determines for sure whether f(x) is positive or negative (for a computable input x), and always completes in a finite amount of time. Perhaps a long time, but finite. A binary search algorithm based on this procedure will eventually determine which half of the search interval to continue searching on. And the number of times the interval needs to be halved only depends on how small you want it to be (i.e. how well you want to approximate x), not on the function itself. So you can approximate the true preimage as precisely as needed in a finite amount of time.
If the input function is not computable then sure, all bets are off...
@@comexk If f maps rational numbers to rational numbers and it is the case that if the input is given as a/b for integers a and b, then you can compute integers c and d such that the output is c/d, then indeed I think the proof goes through constructively. There are certainly other conditions which guarantee that the algorithm works.
However, your I don’t agree with your more general claim that „if f is computable, then there is a procedure that determines whether f(x) is positive or negative (for computable input).“ That depends on what you mean by computable, and how you encode real numbers. Again, if computable means something like in the first paragraph, ok. For instance, x \mapsto x - sqrt(2) is zero iff the input is sqrt(2), so determining whether the function vanishes is equivalent to deciding whether the input is sqrt(2), which is undecidable. (For me, if nothing else is said, real numbers are encoded as infinite sequences of 0 and 1 (and ,) interpreted as binary numbers, and a real function is computable when there is an algorithm that determines the first n digits of the output given a sufficiently large number of input digits.)
For the specific application at hand, one does not actually need all computable inputs, but only rational inputs, as you pointed out. Indeed, for any function f whatsoever, there is a procedure which determines for a pair of integers (a, b) whether f(a/b) = 0. This procedure does not computably depend on the input, therefore I think this is not constructively a theorem, even if f is restricted to be computable. I cannot currently give a more formal argument.
At any rate, it is true constructively that for every n, there is a c_n such that abs(f(c_n)) < 1/n. But this does not allow you to approximate a root to arbitrary precision, because the c_n might be approximations for different zeros. The problem admittedly only occurs for functions whose zero-set has a limit-point, so there is some hope (even though this observation does not help numericists with the problem I pointed out).
iirc, the incomputability of the sign function in R is the only thing that makes it impossible to use R on a computer ( even if you assume infinite memory ), as it's equivalent to making comparison impossible, and i think comparison always ends up being necessary to implement any mathematical operation ( although i forgot the reason. Even if that's not the case, no comparison means absolutely no algorithms )
could you consider things like "constructive mathematics + a real number comparison oracle" to be able to precisely quantify how the first proof is "more constructive" than the second
10:07 the beta formalist forever cries and shivers at the sight of the constructivist KING exuding such levels of facts and logic
In my case, "I didn't dislike" means "I liked and subscribed" ! Really cool video, loved it !
I am so lost right now. Don't know which I should choose: a math degree or sex.
Sex(A, B) can denote the category of left exact functors between abelian categories A and B.
(What I'm trying to say is, don't choose the math degree.)
@@SheafificationOfG omfg bruh
10:53 As a constructivist mathematician who is supposed to be writing code right now, let me just say: ow.
damn!! i can’t believe you got me to exclude the middle. i read all of kleene and learned intuitionistic first order arithmetic just to be bamboozled into excluding the middle
I don't know why, but your videos don't get to my subscriptions, maybe youtube needs a critical mass of subscribers.
Anyway, you defenetly should continue what you are doing, this is brilliant. I am sure you will find your viewer.
Thanks, this fills me with determination! I'm a pretty new channel, so publicity is hard; I'm glad you didn't dislike the video :^)
I've heard this concept before where a problem has a solution, but that solution can't ever be found.
Does this mean the proofs for existence were of the form: "the problem can't not have a solution" ?
Yeah, non-constructive proofs of existence are essentially just proving the impossibility of non-existence. Not worrying about actually providing an example keeps a lot of options open for an elegant or short proof.
For example, it's not a difficult exercise to prove non-constructively that transcendental numbers (numbers that are not solutions to polynomial equations with integer coefficients) exist: you can do it by proving that algebraic numbers are countable, but the set of real numbers is uncountable. This proof demonstrates that, in fact, *most* real numbers are transcendental (i.e., if you randomly sample a real number in [0, 1], you have a 100% chance of drawing a transcendental number). However, the proof is non-constructive; it's really just showing that it's impossible for algebraic numbers to account for all real numbers.
On the other hand, it takes considerably more work to prove that a specific number (e.g., pi or e) is transcendental.
Moment I saw the title I wondered if constructivism would show up. The nonstandard analysis proof of this makes the non constructivism obvious btw
Hard to say constructivism isn't inevitable when you're looking for an algorithm.
You should do a follow up video on The Bolzano-Weierstrass Theorem and its proofs. Similar! Also it brings into discussion notion of complete spaces.
Bolzano-Weierstrass overlaps nicely with something I have in the oven, so I might add it in as seasoning!
(Pretty sure I replied to this already, but I don't see my own response, so idk if UA-cam is bugging or I'm impatient)
The joke at the end about how a triple negation collapses to negation even in the absence of LEM is priceless. XD
I prefer the dichotomy proof for the Bolzano Weierstrass theorem, and the abstract proof for the IV theorem...
Pure math and physics are the parents of computer science and engineering.
This is bringing me back to my Covid topology class
I would not be surprised if they know how to code... Computer science branched out from pure math.
This was quite funny. Easy subscription from me.
For me... Pure math, not applied math, is the ideal course... Next is computer science if the university doesn't have pure math...
Both do hard proofs anyway...
Don't you also need to prove that every connected open subset of R must be an interval?
While it is certainly true that every connected open subset of R is an open interval, it's not necessary for the abstract proof of the IVT: I only ever need connectivity of the closed interval [a, b], since that is the choice of domain of the continuous function.
@tobiaswolf7996 I‘d differ from Sheafification and say that yes, this is precisely the argument: (1) An interval is connected, (2) the image of an interval is connected, and (3) connected sets are intervals, therefore (T) the image of an interval is an interval. But note that this observation (3) is essentially the example at 7:42.
I anticipated the LEM meme.
Some people anticipated it, some people didn't.
The middle? Some people don't care.
@@SheafificationOfG I can at least tell you I haven't not anticipated it
brilliant
Wow... Pure math...
I can´t quite follow the proof at 6:25 in line 8 because f^−1((f (x0) − ε, f (x0) + ε)) could just be the empty set and then no such δ > 0 would exist
The preimage of the interval (f(x_0) - e, f(x_0) + e) under f is never empty: it always contains x_0.
@@SheafificationOfG nevermind, i was just stupid
i love your videos btw
@@palamedez Thanks fam! And nw, checking for the empty set is something I usually forget to do, so it's good to keep me honest 😉
sequential continuity doesn't always imply continuity ;) see non sequential spaces
Preeetty sure the real number line is a sequential space ;) But yes, you're right in general.
Ah yes... the Brower fixed point theorem for n=1
Brouwer's fixed point theorem is definitely on my radar, we'll see what happens in the future.
chad Schauder fixed point theorem stomps it