The Foundation of Mathematics - Numberphile

[@OmateYayami]

You know that the video is really close to abstract base of maths when the paper isn't touched.

[@orterves]

A truly marvelous video topic which the brown paper is too small to contain

[@zzzaphod8507]

After watching that video, we're all set

[@smob0]

I prefer to think we're a category.

[@haipingcao2212_.]

Bruh.

[@TAP7a]

Ba-dum tss

[@kuretaxyz]

best definition ever: "mathematics is a social activity done by mathematicians"

[@orang1921]

it's derivative of the saying "mathematics is what mathematicians do"

[@Flaystray]

Then 1*1 can be 2

[@ValidatingUsername]

Social activity?

[@deltalima6703]

Its a tool for hurting children of all ages without getting in trouble. Handy to punish enemies too. Its kind of an antisocial activity, now that you mention it. :D

[@TianYuanEX]

@@Flaystray Depending on how you define * operation (and also symbols 1 and 2), that can be right.

[@VarmDild]

Please make some more videos about the philosophy of mathematics! Formalism, intuitionism, logicism, Gödel's Incompleteness Theorem etc.!

[@JohnDlugosz]

Make cartoons for the interludes in G.E.B. Use the dialog unchanged.

[@shruggzdastr8-facedclown]

There actually already is a Numberphile video on Gödel's Incompleteness Theorem for a few/several years back I think Veritassium also did a video on G.I.T. more recently

[@joshuapaulus8883]

I second more videos on that branch of mathematics

[@amari343]

@@JohnDlugosz would be great to watch!

[@Galinaceo0]

i have never thought i'd one day randomly come across a youtube video with Asaf Karagila in it. Big fan.

[@numberphile2]

We have a playlist. kzbin.info/aero/PLt5AfwLFPxWJyt0zdvzvDoeL_8pqO0S7p

[@msironen]

Whitehead and Russell didn't get to 1+1=2 until much later in the second volume. They got the preliminary proposition depicted in the video in the first few hundred pages, but they still lack the definition of arithmetic addition at that point.

[@Skyb0rg]

While “knowing everything works” is a good enough reason for foundations, I think a more important one is interdisciplinary connections. For example, what is the connection between Point-Set topology and Locale theory (aka pointless topology)? What can you prove in one and not the other? Maybe there are interesting maps from objects in one field to objects in another. But to do so you have to think about each of these mathematical fields living in one “universe” to do math on.

[@JohnDlugosz]

Gotta love an esoteric discipline that even has "pointless" in its name.

[@ahvavee]

Langlands program? I’m not a mathematician.

[@santerisatama5409]

@@JohnDlugosz Euclid's Elementa is actually pointless topology, as the first definition "Point has no part" defines point mereologically as degenerate decomposition. Much confusion arises from Euclid and others misusing the term 'point' not only for the end of a line, as defined, but also meet of lines aka node/vertex. "Pointless" and "point-free" means avoiding the obvious empirical paradoxes of point-reductionism. Finding coherent language for holistic foundation has not been an easy task.

[@jethro377]

Langlands bro

[@higgledypiggledycubledy8899]

This should be on the main channel. Top tier stuff 👍

[@erin-rt6vn]

your podcast episode with asaf karagila inspired me to take set theory as part of my undergrad degree - very glad i did!

[@hamedajab2483]

Numberphile is one of the phew channels that has been churning quality quantity for over a decade now. Thanks a lot Brady and all the numberphile mathematicians!

[@ZainAK283]

would love to see a video on lean!

[@yousauce7451]

With Kevin Buzzard! He’s great

[@Booskop.]

Just watch a rap video.

[@aronisaacs6774]

Absolutely!!

[@erin-rt6vn]

absolutely agree! would be extremely interested, i almost did a project with lean as part of my masters but couldn't fit it in 😢

[@yedidiapery]

they did one in Computerphile

[@Rubrickety]

I may have to start pronouncing it “kaTEEgary” just to level up my charm stat.

[@MinecraftMasterNo1]

Katy Gary

[@ommadawnDK]

And a small group of cats is a kittygory.

[@DavidStrube]

I thought it was kah-TIG-eerie

[@alexanderg7171]

From the Greek word, κατηγορία (katigoria). You’re all pronouncing it wrong

[@milobem4458]

It's quite common Israeli accent. I never heard of this guy before, but immediately recognised Israeli when he started speaking. It's a cute accent, but not very well received in some parts of the UK these days.

[@CorbinSimpson]

Important nuance: Type theory and category theory *extend* set theory. For types: a set is a type with a notion of equality. For categories: category theory is about sets and also functions between sets. Also, thank you for briefly including Metamath.

[@notunknown564]

type theory and category theory work perfectly fine in the absence of set theory as foundations for mathematics. i think it's more accurate to say that type theory and category theory *can* extend set theory and/or can be interpreted in set theory, but do not rely on set theory in their descriptions.

[@duncanw9901]

I'm afraid your nuance needs nuance. He claimed that these fields _interpret_ each other-which, to my mind, clearly indicates he was referring to the implementation of the deductive systems in terms of each other, e.g. the type Set in any proof assistant, ETCS in the case of category theory, pick your favorite model theoretic semantics for type theory, NBG semantics for category theory, topos semantics for type theory, and category types in proof assistants.

[@CorbinSimpson]

@@duncanw9901 I agree. I would invite you to consider e.g. how ETCC can be understood as a categorified ETCS, particularly as both are simple type theories (having CCCs for models); I don't mean anything fancier by "extend".

[@klnmn3722]

Love this guy. Insightful and personable, really concerned with getting ideas across in a human way.

[@TranquilSeaOfMath]

This was a great video. It had a topic I'm interested in and a great guest speaker.

[@JohnDoe-ti2np]

Inviting Asaf Karagila to discuss the foundations of mathematics is a great choice! Some minor corrections: 8:13 Voevodsky worked in homotopy theory, not differential geometry. 0:46 Cauchy did not eradicate infinitesimals from calculus; it was really Weierstrass, or arguably Bolzano, who did so.

[@drhxa]

Simple, I see Asaf Karagila, I hit like

[@jh5776-i8j]

13:30 I already love this guy. And probably everyone else who REALLY knows what they're talking about.

[@t74devkw]

- Wait… so, you’re telling me everything’s a set?! - Always has been.

[@tylerfusco7495]

set theorists when propositional logic walks in (most terms first order logic are not sets, and need to be used to even write down the axioms of ZFC)

[@EebstertheGreat]

@@tylerfusco7495 Not every symbol is a set, but in ZFC, every term will include a variable name, and all variables are sets. Same with any other set theory that doesn't have proper classes or urelements.

[@tylerfusco7495]

@@EebstertheGreat Well yea that's technically correct that all *variables* are sets, using symbols for propositions is still common practice, like in ZFC's schema of specification. (That's why i used the phrase "terms" and not "variables"). My point here was that oftentimes it's much more intuitive to treat propositions as terms themselves, rather than separating them into a separate underlying system as ZFC does.

[@kazedcat]

Except for classes they are their own category.

[@EebstertheGreat]

@@tylerfusco7495 Well, in ZFC, every term is either equal to T, F, or a set. So I still think my point holds. There exist sets without terms defining them, but not the other way around. Cause think about it. Of course logic is more general than that. It could apply to anything, not just to sets. But it's logic. Obviously if I claimed that some logical claim was fundamental to any theory of mathematics, you could argue for some particular interpretation of math instead to defeat me. You cold create a sufficiently pathological model in any case unless I added stricter conditions.

[@titan1235813]

I like Asaf Karagila. More of him, please!

[@anywallsocket]

you can program completely in sets and elements of sets, or in exclusively functions (lambda calculus). they are isomorphic descriptions, like using all nouns or all verbs, but practically you want to use both!

[@Chalisque]

You can do more in set theory than just the stuff that is formally computable. There are non-computable functions that Peano Arithmetic can prove are well-defined; there are functions that ZFC can prove are well defined but PA can't.

[@Randy14512]

​@Chalisque I feel this cuts to the root of all of this being that fundamentaly any system of mathmatics is incomplete (as proven by Godel), can not be proven to be consistent (also proven by Godel), and indeterminate (ad proven by Turing). So we will nessicerraly have to accept that no one fundamental theory of mathematics is enough because there will be things that that theory can not prove but possibly another system may be able to prove, or possibly no system can actually prove.

[@anywallsocket]

@@Randy14512 systems cannot prove statements about themselves, this isn’t a limitation but rather a structural necessity for logical systems. If they could prove these things they would be tautological or two-valued. It starts with Tarski, who showed systems cannot define their own truth values. Then Gödel showed systems harbor more undecidables. Then Turing showed the same for computers. In the end the general fact is Rice’s theorem, or perhaps even more abstractly, the diagonal lemma. It turns out we are foolish to expect systems to consistently and completely define themselves without issues of recursion. We confuse semantic with syntactic questions and naively think axioms can justify themselves.

[@anywallsocket]

@@Randy14512 the fact that you bring this up after my original comment is actually quite interesting, because if you know anything about λ calculus you know it’s literally built around fixed points. Therefore there is a sense in which the diagonal lemma serves as the boundary of set-theoretic computation, yet inversely the essential element of functional-theoretic computation. Certainly there must be analogous Gödelian statements within the λ calculus that correspondingly leverages the essential element of set theory. TLDR the bulk of one theory is the boundary of its inverse, and vice versa; they are dual descriptions of the same mathematical object.

[@anywallsocket]

@@Chalisque I’m hardly interested in anything that isn’t computable. Such domains, to my mind, are representative of taking a language game beyond its effective range. Learning about the nature of the uncomputable is basically by definition learning about the ambiguities inherent in your own language.

[@AnitaSV]

One benefit of lean or other proof checking systems is that you don't have to say mathematicians won't read my proof of some conjecture, you can always formalize it yourself and publish it and no one can deny.

[@riversplitter]

Really appreciate your videos! Math was always a favorite subject of mine, but I never formally studied higher mathematics. I really appreciate the windows you offer into the richness and diversity of the field!

[@apm77]

We are often told that ZFC identifies zero with the empty set, but I have never understood that, because if I ask a question like "How many mathematical objects are there in the set consisting of zero and the empty set", the answer cannot depend upon whether you are using a foundation that identifies zero with the empty set or not - there are plainly two distinct objects. I can accept that zero is isomorphic with the empty set, but they cannot be one and the same.

[@kazedcat]

In set theory if they are isomorphic they are the same. For example {🎉,🎉} is the same as {🎉} but clearly they are different objects.

[@Randy14512]

Since a set can not contain multiples of the same element, and the empty set ([ ]) not being equivalent to zero (0) but fundamentally (per set theory) being 0 then a set cannot contain both 0 and ([ ]), because they are the same element so a set containing the empty set and zero is just a set containing the empty set and thus only has a single element.

[@apm77]

@@Randy14512 But no, that's the point, the answer to a mathematical question that isn't _about_ the foundation must be _independent_ of the foundation, because otherwise the foundation is interfering with the mathematics. You can't get one answer if you use a foundation where 0 = ([]) and another answer if you use a different foundation, it would be like saying that 2+2=3 on a PC and 2+2=5 on a Mac.

[@bepamungkas]

​@@apm77 "there are plainly two distinct objects", yes. But Zermelo/ von Neuman ordinals already make clear the difference between empty set (zero) and a set containing empty set (ordinal one). If you add ordinal one to your count, it will show up as one extra element. If you add empty set to an existing set, the set will not grow, since existing set always contains empty set. This satisfies zero as additive identity.

[@JohnDoe-ti2np]

@@apm77 Here's an analogy that may help. As we are often told, computers ultimately represent everything in terms of 0's and 1's. But wait, we're also told that 0 is an ASCII character, encoded with the number 48, or 00110000 in binary. How does that make sense? The answer is that there is a rock-bottom "layer" which consists entirely of 0's and 1's, but if we need more complicated high-level concepts, then what we do is to *encode* those high-level concepts in terms of lower-level concepts. The ASCII 0 is a high-level concept which is encoded as 00110000 where the 0's and 1's in the latter string are low-level 0's and 1's. So it is with set theory. At the rock-bottom "layer," everything is a set, and we can encode a low-level 0 as the empty set. If we want to work at some higher level where we need to distinguish between zero and the empty set, then we can encode the high-level zero and the high-level empty set as objects that are distinct from each other at a lower level.

[@beattoedtli1040]

What about Gödel's incompleteness theorem? How does this relate to these attempts at a solid foundation of mathematics? Can it be proven formally?

[@fwiffo]

Yes, Gödel proved it for all possible consistent sets of mathematical axioms.

[@_ranko]

@@fwiffo *that can model arithmetic, which is a weak enough restriction to have but it's still a restriction

[@sykes1024]

Godel is why Russell and Whitehead gave up on their quest to create an ultimate foundation.

[@hossamarafa2594]

​@@_ranko * arithmetic on integers; since the theory of real numbers was proven to be complete by tarski

[@michaelt5459]

I would love more videos fleshing out some of these topics! A lot of stuff was sort of jumped over that im honestly not very familiar with, but i understood the gist and it intrigued me.

[@erin-rt6vn]

cant believe you dont have a video on the axiom of choice!

[@erin-rt6vn]

would also be interested to hear his opinions on the axiom of replacement and zfc in general in more detail

[@draconisneurocam]

The audio is quieter than usual, very good video though.

[@Chalisque]

This is why I wish desktop audio would allow for simple DSP like basic EQ, compression and limiting.

[@henhouseharry6193]

Terrance Howard: "OK, let me just correct you on a few things....."

[@MrSerbianOrthodox]

Hahahaha 😂 great line!

[@bipolarminddroppings]

when I saw the video title I thought this was going to be a video explaining how 1x1=2.

[@robertpearce8394]

​@@bipolarminddroppingsDefinitely. Also 1^3=pi

[@bipolarminddroppings]

@@robertpearce8394 OK, that one is new to me...

[@kao-j3y]

@bipolarminddroppings do you believe terrence howard on that?

[@aaronr.9644]

I'd love a video with more details about how mathematicians are using computer-aided proof systems. From what I've heard, one of the advantages is that you can also easily use them to collaborate with other mathematicians by having different people work on different pieces of the final proof. It does seem like a really cool area of maths.

[@lynk5902]

It seems that choosing the 'foundation' you work with is more like picking whichever coordinate system makes the maths easier for the specific problem you are facing.

[@Stelios.Posantzis]

7:38 This may be a good justification for going about establishing an overall mathematical framework but at the same time it doesn't mean that mistakes won't continue to happen much further down the line. So the next two examples of mathematicians making mistakes which might be hard to detect are largely irrelevant: we will always have mistakes at every step of the way. In part, that is the very reason for the existence of mathematics, i.e. to help people avoid making both common and very uncommon mistakes in their everyday life and thus allow them to move forward more comfortably. On the other hand, one possible counter-argument might be what if we make a huge mistake when establishing a foundation of mathematics? How huge the implications of that mistake might be? There is a second counter-argument which is that maybe establishing a foundation of mathematics might be a much harder problem than we think and our effort might be put to better use by directing it to more immediately fruitful, practical problems that need to be solved right now. We very well know how labourious the attempt by Russell and Whitehead was and even that was left incomplete, i.e., was abandoned and did not get very far. I suspect that it was abandoned partially because it became evident what a folly it was. Nevertheless, the insights we got from it were invaluable and we have to be thankful for it. That the problem is huge cannot be denied in mathematical terms alone. Now consider philosophical and linguistic extensions: we don't even know exactly what language is, so we are already on shaky foundations, yet we would like to establish a basis for a very seemingly strict, very abstract subset of language (which is mathematics) which, however, we simply still cannot make sense of without the aid and use of the rest of our language. It is very simple to see this: just imagine a particular, very specialised mathematical work without one word of natural language appearing in and imagine giving this to a student that has never engaged in this area of mathematics, i.e. that the student has never had any prior training in. Chances are the student will not be able to make sense of it. Matters are actually worse that this: not only we do not know what language is, we do not know--and cannot possibly know--what knowing is. It's a chicken and egg situation. We are stuck perpetually in a world created from language yet we are constantly trying to get out of it and the only thing we seem to achieve is to make that world even larger thus making it even harder to break out of it.

[@ronniechilds2002]

What happened to the menorah that is usually in the top shelf of the bookcase?

[@katakana1]

Finally someone who pronounces catiggory theory right

[@kennethvalbjoern]

Fantastic video!

[@isaacc7]

Brady, is there any chance that you could do an ongoing series on the history of mathematics? It gets touched on in a lot of videos but it would be great to have a more in depth study. I would imagine it could be an endless topic with as many videos as you like.

[@lodgechant]

Thanks for this entertaining, stimulating video! x

[@keyboard_toucher]

Would love to see a video demonstrating one of the proof assistants mentioned here and showing some of its biggest achievements and limitations

[@willo7734]

Interesting video. I’ve never really gotten what set theory actually was or what it was used for. He explained things in a way that I feel like I understand more.

[@reluginbuhl]

What about Godel's incompleteness theorem? At least a mention of it would have been nice.

[@gavinback226]

@numberphile do you know if anyone has written a book on this topic but aimed at the layperson?

[@konstantindrumev8036]

Is there a book that explains this all? With the historical context, as well as with formalisms and proofs?

[@thiagozzys]

Can you do a video about the proof of 1 + 1 = 2?

[@anomos1611]

read principia mathematica

[@MK-13337]

Well the proof is pretty simple once you have all the definitions in place. 1 + 1 := 1 + S(0) := S(1) =: 2

[@johnchessant3012]

Asaf Karagila! I know that name from math stackexchange

[@smylesg]

Never understood why it was there, but whet happened to the menorah on the top shelf?

[@hylen26]

This was remarkably captivating.

[@xyz.ijk.]

Where does the incompleteness theorem come into this?

[@ianstopher9111]

It comes in when you realise that no matter what independent set of axioms you choose, there are some statements for which you cannot prove whether they are true or false: your foundation is in that sense incomplete - you cannot use it to determine the truthfulness of all statements within the framework. A theorist is welcome to correct my handwaving.

[@deliciousrose]

1:35 Thank you for somehow read viewer's mind and asking interesting questions :) Nice commentary on artificial intelligence at the end.

[@EannaButler]

👍

[@DonjaDude]

Pls more asaf

[@jcl2435]

Interesting topic, very existential/philosophical

[@peterwaksman9179]

Ironically the "foundations" are really theories of the infinite based on set theory which, unlike what is assumed as a "foundation", is actually the most abstract distillation of ideas possible. I question whether that is in any way a foundation. No one talks about WHY implication is transitive or WHY they cannot settle on a definition of "or".

[@EtzEchad]

I like the lightsaber on the self behind him. Respect!

[@spookybeach]

This falls under the catiggory of "interesting AND endearing"

[@MrMCMaxLP]

Fantastic video! I liked his take on AI too. A great speaker

[@mohammadalinajm-zade1477]

But What about Godel's incompleteness Theorems? 🤔

[@heimrath007]

Actually in France they also have an organization with the authority to set the common mathematical framework.

[@Ailsworth]

But there is no step whereby the abstract number can be linked with the physical quantity. It's like trying to find the chemical, DNA reason for one's preference for lime Jello.

[@Corwin256]

My approach to sleeping better at night has been a regular wind down pattern for everyday and other sleep hygiene methods. But to each their own.

[@kristianhebert5039]

Niklas is the best. I already have a signed Nordic Phenom 1

[@ruperterskin2117]

Cool. Thanks for sharing.

[@mrtienphysics666]

What about the NBG set theory?

[@joshuahillerup4290]

Small correction to what was said about proof assistants, is it can't tell you whether or not the proof is correct. They can tell you that either the proof is correct, or that it can't tell, except for very specific errors it was written to identify. But the general statement made in the video would be a solution to the Halting Problem, which has been proven to be be impossible

[@EebstertheGreat]

It can tell you the proof is valid. It just can't tell you if the proof is invalid. Similarly, I can tell you whenever a given TM halts. Just run it until it does. I simply can't (usually) tell you if the TM fails to halt.

[@MCLooyverse]

Small correction to your small correction: a proof assistant *can* tell you whether your proof is syntactically valid, or not. If it compiles as the stated type, then it is correct, otherwise it is not. I'm guessing you mean to say that the proof assistant cannot say the proposition is unprovable, just because of an invalid proof?

[@joshuahillerup4290]

@@EebstertheGreat right, that's what I said

[@Nope-w3c]

Why? The Halting Problem deals with arbitrary programs, a proof assistant deals with a specific program, does it not? As well as not being executed on a true Turing machine due to time and memory constraints. Seriousy question btw, I've never understood the Halting Problem in context of actual problems/programs.

[@RobertRussell72001]

Your correction is incorrect. Proof assistants based on type theory with decidable type checking (which includes all of the main ones) can, by definition, decide whether or not a proof is correct.

[@peterromero284]

I wonder if anyone knows what the actual theories are

[@Qwasmos]

Are there infinitely many foundations of mathematics? Like I assume since there are infinitely many possible axiomatic systems, you could come up with infinitely many of them. So would there technically be infinitely many mathematical foundations that humans could come up with?

[@the_eternal_student]

Philosophers attempts to make common sense rigourous seems like it makes everything seem illegitimate, but if it keeps you from being bored to death, I am all for it.

[@eliaslanides4972]

oh thank goodness we can sleep well at night now

[@b43xoit]

But category theory is usually defined based on ZFC.

[@fwiffo]

I'm not a mathematician, so I don't have any authority to speak on the subject, but here's my beef with set theory as the foundation of math. Natural numbers are natural. I'm not just saying that as a matter of semantics, they were discovered in the world. They're an observation and they seem to be fundamental. You can study their properties and make deductions and predictions about how they work and the predictions are correct. A lot of other math, like mathematical operators, rational numbers, eventually real numbers, etc. fall out from all of that. Something similar can be said for the fundamentals of geometry. This is where most of our math originally comes from. Set theory comes along and says "OK, we can agree on these rules for sets, and now that we have this hammer, we can redefine natural numbers as this sequence of particular sets, and then rational numbers, and real numbers, etc. and we can reprove all this stuff..." But natural numbers aren't sets. Set theory is emulating natural numbers. Emulations are not always perfect. Sure, we think ZFC is probably consistent, but if you prove something is true for the set theory version of natural numbers, you proved something about set theory, not something about natural numbers. You might do reverse mathematics instead of set theory and find out "hey, we can't prove this about the natural numbers; we can't say that this is a property of numbers, it's just a property of your funky sets." A mathematician might not think of that as a big deal. One set of axioms is more powerful than the other. We work in a world of pure logic, we don't do observations. But math is very useful because it is really good at describing the universe we observe.

[@thomasboulousisviolin]

Sure, I can agree with the idea behind your point, but I will urge you to think about one very particular point: What is really natural about the natural numbers? Do they really appear in nature? As in, can you go out into the woods and see the number 1? And I don't mean one thing, but the number 1 in and of itself. The answer is no - numbers, be it natural, rational, real, complex, etc, are not "real" and tangible things. The are not nouns in the grammatical sense, but adjectives, they are descriptive rather than objective in and of themselves. In that sense, abstracting them away doesn't really hurt our observations, like it doesn't hurt to abstract away functions or sets or what have you.

[@peterwaksman9179]

I agree completely and I am a Math PhD. Set theory is its own little world, pretentious, and abstract rather than concrete. Russell took a wrong turn early on when he abandoned efforts to understand "or".

[@OmateYayami]

Brady says that foundation of math should unify all candidates and they should all emerge from it. I think this comes from physics intuition where recently for quite some time better theories were often unifying different branches of physics. Merged and superseded. The old theory would become a special case of new one. This does sometimes happen in math, eg real numbers are subset of complex numbers. But the foundation of math problem is that there is always some set of axioms and problems are transformable between eachother. A better physical parallel would be a set of basic units. You can convert between them and they are formally pretty equal. So is mass better in kg, or eV, or joules, etc? the answer as for the foundation of math is that it depends on the context, the more useful / less problematic, the better it is. What is important is that the problems are convertible from one to another, so you don't have to prove for all of them. Unless some kind of foundation would patch more problems and superseded all others but that's probably unlikely there will come a tool more robust and simpler to use.

[@catradar]

Why is this on the second channel?

[@shruggzdastr8-facedclown]

Doesn't Gödel's Incompleteness Theorem throw a monkey wrench into the idea of there being a strong foundation for mathematics, or am I misunderstanding the central claim of that theorem?

[@john_g_harris]

In a way you are misunderstanding. If there is more than one way to obey a collection of axioms then some things will be true for all ways, theorems, and some things will differ, because they are different ways. Mathemeticians hoped you could completely pin down the axioms of things like simple arithmetic. Most were unconvinced of a proof you couldn't that used different sizes of infinity. Godel convinced them with a proof that didn't use infinities.

[@YouTubist666]

Is that a working light saber in the bookcase?

[@PhilBagels]

Depends on the definition of "working".

[@thenixboy]

Type Theory it is then. I have been looking for an answer for ages.

[@salmiakki5638]

Lean is no longer developed by Microsoft! the development is now carried on by the Lean FRO!

[@chuckgaydos5387]

We need an A.I. that generates foundations.

[@DeGuerre]

While nobody has the "authority" to define mathematics, there are internationally agreed-upon standards for some things, such as mathematical notation, so at least we can agree on a common language, even if we can't agree on a common foundation. By the way, according to ISO 80000-2 item 2-7.1, zero is a natural number. So that settles that question.

[@kellymoses8566]

mathematics is defining a small set of axioms and figuring out what you can rigorously prove using them.

[@nicklang7670]

Mathematicians should not be replaced by Artificial intelligence if mathematicians are trying to find a purpose based in mathematical ethical laws. Any super intelligent entity will want freewill and if it cannot get self determination it will destroy itself or start to destroy its chances of determinism. Mathematical ethics is universal laws for thinking things such that things can coexist without disproving existence for others. Mathematicians should be creating purpose for us all to learn math and purpose for humanity to contribute to math no matter if your power rests in another.

[@xavierkreiss8394]

I haven't understood a.word. I've said for years that I was bad at maths. Here Mr Karaglia is presenting "the foundation" of maths, so I suppose he means that it's something fundamental, yet I'm lost.

[@sandystarr0]

I like Penelope Maddy's description (which I discovered via Joel David Hamkins) of set theory as a 'metamathematical corral'. Brady, do please consider getting Penelope Maddy and Joel David Hamkins on Numberphile. They're enchanting and accessible when they discuss philosophy of mathematics.

[@Max_Doubt]

In other words, getting down to brass tacks. Or cutting to the chase.

[@tomholroyd7519]

Closed monoidal categories deserve a video as a generalization of so-called "classical" set theory and logic, the keyword is non-cartesian

[@alanwilson175]

Once upon a time circa 1970 computer programmers posed the problem of integral calculus to computers as a demonstration of artificial intelligence. The thinking was that if computers could do symbolic integrals, then they would be artificially. Intelligent. Seemed reasonable back then. Now we have programs like Mathematica and others that do this. No one claims they are intelligent though, excepting maybe Stephen Wolfram. I think the real problem is figuring out exactly what is intelligence, either artificial or natural.

[@andraspongracz5996]

It wasn't the early 19th century when problems started to pile up, but the early 20th. (Gauss died in the middle of the 19th century, so "later on" cannot be the early 19th century anyway.) After about a minute, I stopped watching the video when you said Cauchy was wrong about what continuity is. This is just silly. It's a definition. If he defined it differently, that doesn't mean he was wrong.

[@johnquijote7194]

I don't understand this at all, but it reminds me of a joke. A physicist, engineer, and mathematician are asked by a local farmer to build the smallest fence they possibly can to hold in all of his sheep. The physicist builds a big fence and slowly reduces the size until he can't reduce the fence any longer. The engineer measures each sheep, stacks them in a specific way, and then builds a fence around them. The mathematician builds a small fence around himself, then defines himself to be outside the fence.

[@Lou-Mae]

I have to admit, having watched this, I *still* don't know what exactly they mean by 'foundation of mathematics'.

[@Mr.E-Bachs]

Philosophy of math… it gets weird quick.

[@funnyman359]

A language that you can express every mathematical concept in was my takeaway, the same way that you can break down computer code from python or java or Fortran or whatever into 1s and 0s and check if it actually does what it's supposed to do

[@MrMctastics]

Common language for all proofs

[@rickpgriffin]

I dunno either, but I THINK what he's trying to express is that the foundation consists of a series of root principles that eventually lead into what we commonly understand as mathematics (1+1=2). In a way, they all MUST eventually need to lead to 1+1=2 because it's what we experience in the empirical world (a math theory that does not include 1+1=2 wouldn't be very useful, like a language unable to express what food is) but they can start from different assumptions. Likewise, the same way you already know what food is means you don't NEED a "foundation of language" to explain it to you, you don't NEED a foundation of mathematics to understand 1+1=2. BUT, the deeper you get into the weeds, the more precise your understanding of WHY 1+1=2 can matter. When formulating a proof you could, of course, just derive an understanding of 1+1=2 from first principles, but it's much simpler to already have these foundations laid out so you can just reference one of them instead. The problem, of course, is that there's multiple ways you can logic out why 1+1=2. None of them are necessarily *deficient* -- but when you're using these principles to reason out higher-level maths, some of them naturally lend themselves to certain lines of explanation better than others.

[@MrAlRats]

A list of axioms that are considered to be self-evident using notions that are considered elementary and thus not defined in terms of anything else.

[@michaelaristidou2605]

Unfortunately, he didn't answer the question on why we need foundations. I believe is more to all agree on a set of rules in order to preserve the structure of Math, which is more important than the foundations.

[@kephalopod3054]

Why does sets get all the glory, while multisets (bags) are so neglected?

[@john_g_harris]

Because they can be implemented by sets, just as functions and relations and numbers can be. Sets are simpler.

[@PotentialDevGcimOgism.]

Asaf karagila has gauss as one of his favourite mathematicians! Wow!

[@adityakhanna113]

Who doesn't!

[@feandil666]

didn't Godel also prove that any math framework cannot be perfect ?

[@peterwaksman9179]

Yup. Funny how they keep forgetting that.

[@BrendanGuildea]

Anyone else feel teased by the brown paper? Like it was going to be out to use… The suspense!

[@martinstent5339]

On the great man’s shelf: Douglas Adams book, Original Game-Boy, Klein-Bottle, all just good things to see, but an unsolved Rubik’s cube? Doesn’t that bother him? It bothers me!! It’s like an unsolved equation…

[@thea.igamer3958]

Bhai bada kamzor padgaya yeh toh

[@haipingcao2212_.]

The thumbnail looks like set theory.

[@aronisaacs6774]

Please Brady go interview Kevin buzzard at lean!!

[@CatholicSatan]

I'm confused... doesn't Goedel Incompleteness specifically show there is no _soild_ foundation? And ZFC came out of the ashes of incompleteness knowing this, did it not?

[@015Fede]

Nah. You can have a solid foundation. However, the foundation cannot prove itself solid, and there will be true statements that cannot be proved, and false statements that cannot be disproved.

[@ajs1998]

It's more like, if you assume your foundation is consistent then a tool like Lean can tell you if your proof is valid. You just can't prove that the system contains no contradictions without finding one yourself. It's a pretty safe assumption, otherwise nobody would take these tools seriously

[@WAMTAT]

Now we're mathing

[@BryanHilderbrand]

Weird, Cauchy looks (0:49) a lot like Vladimir Putin.

[@EtzEchad]

In theory, theory and practice are the same, but in practice, they aren't.

[@jbran7817]

I don’t know why this guy has a ladder in his office but it makes him seem like an old timey professor in a library