18 ms·
A new bridge links the math of infinity to computer science
- k_bx 10mo ago> All of modern mathematics is built on the foundation of set theory, the study of how to organize abstract collections of objects What the hell. What about Type Theory?
- School-Cotton 10mo ago"the study of how to organize abstract collections of objects" is not really a great explanation of set theory. But it is true that the usual way (surely not the only way) to formalize mathematics is starting with set-theoretic axioms and then defining everything in terms of sets.
- k_bx 10mo ago"Usual", "most common by far" etc. are all great phrases, but not "all of mathematics", esp when we talk about math related to computer science
- School-Cotton 10mo agoMath related to CS is typically formalized starting with set theory, just like other branches of math.
- A_D_E_P_T 10mo agoWhat's important to note is that this is just a matter of convention. An historical accident. It is by no means a law of nature that math need be formalized with ZFC or any other set theory derivative, and there are usually other options. As a matter of fact, ZFC fits CS quite poorly. In ZFC, everything is a set. The number 2 is a set. A function is a set of ordered pairs. An ordered pair is a set of sets. In ZFC: It is a valid mathematical question to ask, "Is the number 3 an element of the number 5?" (In the standard definition of ordinals, the answer is yes). In CS: This is a "type error." A programmer necessarily thinks of an integer as distinct from a string or a list. Asking if an integer is "inside" another integer is nonsense in the context of writing software. For a computer scientist, Type Theory is a much more natural foundation than Set Theory. Type Theory enforces boundaries between different kinds of objects, just like a compiler does. But, in any case, that ZFC is "typical" is an accident of history, and whether or not it's appropriate at all is debatable.
- jltsiren 10mo agoIn CS, types are usually a higher level of abstraction built on top of more fundamental layers. If you choose to break the abstraction, you can definitely use an integer as a string, a list, or a function. The outcome is unlikely to be useful, unless your construct was designed with such hacks in mind. When I did a PhD in theoretical computer science, type theory felt like one niche topic among many. It was certainly of interest to some subfield, but most people didn't find it particularly relevant to the kind of TCS they were doing.
- School-Cotton 10mo agoSure, but it fits the rest of mathematics "poorly" for exactly the same reasons. No working mathematician is thinking about 3 as an element of 5. The reason ZFC is used isn't because it's a particularly pedagogical way of describing any branch of math (whether CS or otherwise), but because the axioms are elegantly minimal and parsimonious.
- k_bx 10mo agoSorry but if you try to prove 2+2=4 in ZFC versus Type Theory (HoTT-style) – nothing looks elegant about ZFC afterwards.
- rdlw 10mo agoIs there a collection of type theory axioms anywhere near as influential as ZF or ZFC?
- k_bx 10mo agoSure, but is discarding Type Theory and Category Theory really fair with a phrase like "All of modern mathematics"? Especially in terms of a connection with computer science.
- anon291 10mo agoArguably, type theory is more influential, as it seems to me all the attempts to actually formalize the hand-wavy woo mathematicians tend to engage in are in lean, coq, or the like. We've pretty much given up on set theory except to prove things to ourselves. However, these methods are notoriously unreliable.
- nathias 10mo agothe empirical modern mathematics are build on set theory, type and category theory are just other possible foundations
- A_D_E_P_T 10mo agoMost modern mathematicians are not set theorists. There are certain specialists in metamathematics and the foundations of mathematics who hold that set theory is the proper foundation -- thus that most mathematical structures are rooted in set theory, and can be expressed as extensions of set theory -- but this is by no means a unanimous view! It's quite new, and quite heavily contested.
- nathias 10mo agoyes of course, I just mean that from the set of foundational mathematics, set theory is the strongest one empirically, but that there are other options (possibly better)
- housecarpenter 10mo agoMy impression (as a dilettante programmer without relevant credentials) is that there isn't really any question about whether mathematical structures can be rooted in set theory, or can be expressed as extensions of set theory. Disputes about foundations of mathematics are more about how easy or elegant it is to do so. (And in fact my impression is they're mostly about subjective, aesthetic considerations of elegance rather than practical considerations of how hard it is to do something in practice, even though the discussion tends to be nominally about the practical side. Quite similar to disputes about programming languages in that respect.)
- deleted 10mo ago[deleted]
- philipfweiss 10mo agoType theory is actually a stronger axiomatic system than ZFC, and is equiconsistent with ZFC+ a stronger condition. See this mathoverflow response here https://mathoverflow.net/a/437200/477593 https://mathoverflow.net/a/437200/477593
- deleted 10mo ago[deleted]
- BalinKing 10mo agoTo echo the sibling comment, that answer is specifically referring to the type theory behind Lean (which I’ve heard is pretty weird in a lot of ways, albeit usually in service of usability). Many type theories are weaker than ZFC, or even ZF, at least if I correctly skimmed https://proofassistants.stackexchange.com/a/1210/7 https://proofassistants.stackexchange.com/a/1210/7.
- zozbot234 10mo agoRegardless of the name, descriptive set theory does not seem to have all that much to do with "set theory" in a foundational sense; it can be recast in terms of types and spaces with comparative ease, and this can be quite advantageous. The article is a bit confusing in many ways; among other things, it seems quite obviously wrong to suggest that recasting a concept that seems to be conventionally related to mathematical "infinities" in more tangible computational terms is something deeply original to this particular work; if anything, it happens literally all the time when trying to understand existing math in type-theoretic or constructive terms.
- shevy-java 10mo agoFinally - we can calculate infinity. Been a long way towards it. \o/
- anon291 10mo agoFairly trivial, in haskell: let x = x in x Completely encapsulates a countable infinity.
- firecall 10mo ago>Finally - we can calculate infinity. And Beyond!
- Nevermark 10mo ago∞/1 + 1/∞ One infinitesimal step for the numerical, one giant step for mathkind.
- gorgoiler 10mo agoIf you’re in the Bay Area next month then The Dillinger Escape Plan are bringing the Calculating Infinity circus to town(s): https://www.theregencyballroom.com/events/detail/?event_id=1164123 https://www.theregencyballroom.com/events/detail/?event_id=1... This is enormously off topic but if one person sees this and ends up not missing the show then it was worth mentioning. I think there’s a reasonable crossover between math, discrete math, hacking, and mathcore :)
- anthk 10mo agoIt's cons'es all the way down.
- anon291 10mo ago> computer science with the finite um... no... computer science is very concerned with the infinite. I'm surprised quanta published this. I always think highly of their reporting.
- awesome_dude 10mo agoInitially I too thought - but we try to approximate infinity in CS all the time. But I have come to think, well actually, approximate is doing some heavy lifting there AND I have never used infinity for anything except to say "look I don't know how high this should go, so go as far as you can go, and double that, which is really saying, you are bound by finite boundaries, you'll have to work within them, and the uncountable thing that I was thinking about is really finite. Edit: Think of it like this We know that it's most likely that the universe is infinite, but we can only determine how big it is by how far we can see, which is bounded by the speed of light, and the fact that we can only see matter emitting light (I'm being careful here, if the big bang theory is right, and I am understanding it correctly, there is a finite amount of matter in the universe, but the universe itself is infinite)
- zmgsabst 10mo agoAsymptotics is a good example of CS using infinity practically. Also, a small aside: there’s a finite amount of matter in the visible universe. We could have infinite matter in an infinite universe.
- shwaj 10mo agoAnother glaring example: > Set theorists use the language of logic, computer scientists the language of algorithms. Computer science doesn’t use logic? Hello, Booleans. So lazy, especially when you can ask an AI to tell you if you’re saying something stupid.
- chemotaxis 10mo agoI think this is pretty common for Quanta, and it might be sticking out more because it's a field we're familiar with. I'm really torn about this, because I think they're providing a valuable service. But their general formula doesn't diverge a whole lot from run-of-the-mill pop-science books: a vague, clickbaity title and then an article that focuses on personalities and implications of discoveries while glancing over a lot of important details (and not teaching much).
- alexnewman 10mo agoI studied math for a long time. I’m convinced math would be better without infinity. It doesn’t exist. I also think we don’t need numbers too big . But we can leave those
- dumstick 10mo agoIs this a joke or are you deeply interested in some ZFC variant that im unaware of? We absolutely need infinity to make a ton of everyday tools work, its like saying we dont need negative numbers because those dont exist either.
- zozbot234 10mo agoA ZFC variant without infinity is basically just PA. (Because you can encode finite sets as natural numbers.) Which in practice is plenty enough to do a whole lot of interesting mathematics. OTOH by the same token, the axiom of infinity is genuinely of interest even in pure finitary terms, because it may provide much simpler proofs of at least some statements that can then be asserted to also be valid in a finitary context due to known conservation results. In a way, the axiom of infinity seems to behave much like other axioms that assert the existence of even larger mathematical "universes": it's worth being aware of what parts of a mathematical development are inherently dependent on it as an assumption, which is ultimately a question of so-called reverse mathematics.
- fellowmartian 10mo agoThere’s tons of variants of ZFC without the “infinity”. Constructivism has a long and deep history in mathematics and it’s probably going to become dominant in the future.
- nighthawk454 10mo agoThere are a couple philosophies in that vein, like finitism or constructivism. Not exactly mainstream but they’ve proven more than you’d expect https://en.wikipedia.org/wiki/Finitism https://en.wikipedia.org/wiki/Finitism https://en.wikipedia.org/wiki/Constructivism_(philosophy_of_mathematics) https://en.wikipedia.org/wiki/Constructivism_(philosophy_of_...
- dboreham 10mo agoConfused why the article author believes this is a surprise. The foundations of mathematics and computer science are basically the same subject (imho) and dualities between representations in both fields have been known for decades.
- deleted 10mo ago[deleted]
- kadoban 10mo agoIt's not a surprise that math and CS are related. It's a surprise that this particular subject in math and CS are so intimately related.
- zmgsabst 10mo agoIs it? The notion of algorithms and computer science were invented to discuss the behavior of infinite sequences: examining if there’s descriptions of real numbers. This was extended by connecting complicated infinite structures like the hyperreals with decisions theory problems. That descriptions of other infinite sets also corresponds to some kind of algorithm seems like a natural progression. That it happens to be network theory algorithms rather than (eg) decision theory algorithms is worth noting — but hardly surprising. Particularly because the sets examined arose from graph problems, ie, a network.
- a_tartaruga 10mo ago> He wanted to show that every efficient local algorithm can be turned into a Lebesgue-measurable way of coloring an infinite graph To me this is quite surprising. Distributed systems were not designed to solve measure theory problems.
- jsrozner 10mo agoPerhaps it’s that a global solution in the language of set theory was hard to find, but distributed systems — which need to provide guarantees only from local node behavior, without access to global — offered an alternate perspective. They weren’t designed to do so but they ended up being useful.
- donw 10mo agoThat’s nothing, ‘node_modules’ has been linking the math of infinity to my filesystem for years.
- tug2024 10mo ago[dead]
- deleted 10mo ago[deleted]
- md224 10mo agoThis might be a dumb question but are there any current or foreseeable practical applications of this kind of result (like in the realm of distributed computing) or is this just pure mathematics for its own sake?
- anonymousDan 10mo agoNot a dumb question. The links to mesh networking etc seem interesting. It sounds like the insights from descriptive set theory could yield new hardness/impossibility results in computational complexity, distributed algorithms etc.
- lupire 10mo agoare there any current or foreseeable practical applications of those results? the math of infinity isn't very relevant to the finite programs that humans use. Even today's astronomically large computing systems have size approximately equal to 3 compared to infinity.
- FilosofumRex 10mo agoOne, in theory, can construct number sets (fields) with holes in them - that's truly discrete numbers. such number sets are at most countably infinite, but need not be. One useful such set might have Planck's (length) constant as its smallest number beyond which there is a hole. The problem with using such number sets is that ordinary rules of arithmetic breakdown, ie division has to be defined as modulus Planck constant
- drdeca 10mo agoSuch a thing would not be a field. You can define an additive group $\frac{1}{n}\mathbb{Z}$ if you like. However (for $n > 1$) it would not even be a ring, because it would not be closed under multiplication. (It's closure under multiplication would be $\mathbb{Z}[\frac{1}{n}]$, which would not have a smallest positive element, contrary to your design criterion.) (Of course, you could define a partial multiplication on it. I don't think there's a good name for such a thing. I guess you could just call it "a subgroup of the rational numbers under addition, equipped with a partial multiplication operation that is defined and agrees with the usual multiplication on rational numbers when the result would still be in the subgroup")
- FilosofumRex 10mo agoThe field Qp of p-adic numbers is complete with respect to the p-adic norm, but is not ordered in the same sense as field of real numbers. It's still uncountable infinite. If there is a sense in which "gaps" or Holes can be introduced without breaking its completeness, that would make it very useful for modeling reality
- drdeca 10mo agop-adics may be useful, yes, as may other fields. They do not constitute a field with a smallest non-zero element.
- moi2388 10mo agoEmdash all over the article. It wasn’t just that.. all over the article.. I am getting really strong LLM article vibes. …that existed in the world of descriptive set theory — about the number of colors required to color certain infinite graphs in a measurable way. To Bernshteyn, it felt like more than a coincidence. It wasn’t just that computer scientists are like librarians too, shelving problems based on how efficiently their algorithms work. It wasn’t just that these problems could also be written in terms of graphs and colorings. Perhaps, he thought, the two bookshelves had more in common than that. Perhaps the connection between these two fields went much, much deeper. Perhaps all the books, and their shelves, were identical, just written in different languages — and in need of a translator.
- zkmon 10mo agoWhen you talk about infinity, you are no longer talking about numbers. Mix it with numbers, you get all sorts of perplexing theories and paradoxes. The reason is simple - numbers are cuts in the continuum while infinity isn't. It should not even be a symbolic notion of very large number. This is not to say infinity doesn't exist. It doesn't exist as a number and doesn't mix with numbers. The limits could have been defined saying "as x increases without bound" instead of "as x approaches infinity". There is no target called infinity to approach. Cantor's stuff can easily be trashed. The very notion of "larger than" belongs to finite numbers. This comparitive notion doesn't apply to concepts that can not be quantified using numbers. Hence one can't say some kind of infinity is larger than the other kinds. Similarly, his diagonal argument about 1-to-1 mapping can not be extended to infinities, as there is no 1-to-1 mapping that can make sense for those which are not numbers or uniquely identifiable elements. The mapping is broken. No surprise you get weird results and multiple infinities or whatever that came to his mind when he was going through stressful personal situations.
- sabellito 10mo ago> Cantor's stuff can easily be trashed. Only on hackernews.
- zkmon 10mo ago.. because that is where you are allowed to challenge some biblical stories of the math without the fear of expulsion from the elite clubs. Most of math history is stellar, studded with great works of geniuses, but some results were sanctified and prohibited for questioning due to various forces that were active during the times. Application of regular logic such as comparison, mapping, listing, diagonals, uniqueness - all are the rules that were bred in the realms of finiteness and physical world. You can't use these things to prove some theories about things are not finite.
- gloftus 10mo agoThis isn't iconoclasm, it's ignorance.
- xjm 10mo agoFirst sentence: > All of modern mathematics is built on the foundation of set theory That's ignoring most of formalized mathematics, which is progressing rapidly and definitely modern. Lean and Rocq for example are founded on type theory, not set theory.
- jfmc 10mo agoNot a mathematician, but AFAIK ZFC is a valid foundation. Dependent types helps a lot with bookkeeping, but cannot prove more theorems. Lawrence Paulson is a great person to clarify those topics (Isabelle/HOL is not based on types yet it can proof most maths).
- robinzfc 10mo agoIsabelle/HOL is still types. The underlying type theory of Isabelle/HOL is not theory of dependent types, but theory of simple types. Isabelle/ZF would be a better example as it encodes Zermelo–Fraenkel set theory.
- jfmc 10mo agoRight!
- Garlef 10mo ago> but cannot prove more theorems usually you're more interested in better ergonomics: can you do X with less work? it's like picking a programming language - depending on what you're attempting, some will be more helpful. and ZFC is a lot more low level than what day-to-day mathematics usually bothers with. So most mathematians actually work in an informally understood higher-order wrapper, hoping that what they write sufficiently explains the actual "machine code" the idea then behind adopting alternative foundations is that these come with "batteries included" and map more directly to the domain language.
- lupire 10mo ago>hoping that what they write sufficiently explains the actual "machine code" actual, having faith that what they write could compile, run, and pass tests, but never doing so.
- user3939382 10mo agoThat’s nothing wait til you see my math.