5 ms·

I read the article. The significance of the recent mathematical advances, especially topology, is that somebody will be born and combine them into a major adva

I read the article. The significance of the recent mathematical advances, especially topology, is that somebody will be born and combine them into a major advance later. The article is a bit misleading to laypersons in that pure math (topology and countability) and computer science have almost no overlap in the short term. Pure mathematicians don't use computers or even think of them in their work, for the most part. It's up to applied mathematicans to read their proofs and do something concrete later, if applicable.

jhgb 5y ago
> pure math (topology and countability) and computer science have almost no overlap in the short term I may be misinterpreting the word "overlap" since I've seen quite a bit of usage of at least countability in CS works. Did you mean that CS doesn't influence pure math back?
- ogogmad 5y ago
  You mean countability as a term in set theory. How is axiomatic set theory useful in computer science? Axiomatic set theory is a non-constructive theory. Many results in set theory depend on the existence of functions which cannot be computed. Or assert that something exists without providing any means of finding it. Even the Cantor-Schroeder-Bernstein theorem asserts the existence of something that cannot be explicitly constructed. I fail to see how any of it has any connection to computing. More broadly, I think many computing people are too uncritical about the relevance of mathematics like AST to their discipline. They are very likely to find themselves disappointed.
yakubin 5y ago
> Pure mathematicians don't use computers or even think of them in their work, for the most part. That's not true. Many pure mathematicians use programs such as Wolfram Mathematica and Macaulay2 in their work. (Source: I studied maths and I know a bunch of them personally.)
- ogogmad 5y ago
  Agreed. The OP's assertion is questionable. I don't know how good of a mathematician I am, but I've certainly used computers in all sorts of ways: CAS, plots, numerical experiments, wikis/blogs/QA sites... You use whatever you can. Proof assistants are having a bit of a breakthrough as well, while previously they were associated with "inelegant" proofs or non-mainstream stuff for mathematicians. Mandelbrot talked about an anti-computer snobbery that permeated mathematical culture in university mathematics departments in the '70s, and how he overcame it and produced the famous Mandelbrot set.
sixbrx 5y ago
Might want to read the "Math and Computers Join Forces" near the end. Includes a use of interactive theorem prover Lean (functional language with a dependent type system) and some other stuff. Very much CS meets math.
wittycardio 5y ago
Theoretical Computer science is math
- ogogmad 5y ago
  The word "math" means different things to different people. It makes discussing the relevance (or not) of mathematics to computing difficult.
liups 5y ago
> pure math (topology and countability) and computer science have almost no overlap in the short term. This is an unexpected opinion. What do you mean by this? I would argue the opposite. Look at Formal Verification[0]. Here's a great video about a popular formal verfication proof assitant: https://www.youtube.com/watch?v=Dp-mQ3HxgDE https://www.youtube.com/watch?v=Dp-mQ3HxgDE A quote from the mathematician in the video expressing enthusiasm for using computers for mathematics: "All I want to do... I don't want to do mathematics on pen and paper anymore, because I don't trust it, and I don't trust other people that use it; which is everyone." (in case people only read this quote, instead of watching the lecture, the tone is tongue-in-cheek) Formal Verification would seem a literal intersection of pure math (formal proofs[1]) and computer science (formal specification[2]). Of note, one of the popular underlying foundations of an approach to formal verification is Homotopy Type Theory(HoTT)[3][4] which is an asserted effort to show the relationship between type theory and, specifically, topology (homotopy[5]). [0] https://en.wikipedia.org/wiki/Formal_verification https://en.wikipedia.org/wiki/Formal_verification : fancy word for 'computer verified mathematical proofs' [1] https://en.wikipedia.org/wiki/Formal_proof https://en.wikipedia.org/wiki/Formal_proof : fancy word for 'proof' [2] https://en.wikipedia.org/wiki/Formal_specification https://en.wikipedia.org/wiki/Formal_specification : fancy word for 'rules for an algo that checks a proof' [3] https://en.wikipedia.org/wiki/Homotopy_type_theory https://en.wikipedia.org/wiki/Homotopy_type_theory [4] https://homotopytypetheory.org/book/ https://homotopytypetheory.org/book/ : a great read, even if you are a novice, or prefer other formal verification foundations [5] https://en.wikipedia.org/wiki/Homotopy_theory https://en.wikipedia.org/wiki/Homotopy_theory : "It originated as a topic in algebraic topology"

jhgb 5y ago

> pure math (topology and countability) and computer science have almost no overlap in the short term I may be misinterpreting the word "overlap" since I've seen quite a bit of usage of at least countability in CS works. Did you mean that CS doesn't influence pure math back?

ogogmad 5y ago
You mean countability as a term in set theory. How is axiomatic set theory useful in computer science? Axiomatic set theory is a non-constructive theory. Many results in set theory depend on the existence of functions which cannot be computed. Or assert that something exists without providing any means of finding it. Even the Cantor-Schroeder-Bernstein theorem asserts the existence of something that cannot be explicitly constructed. I fail to see how any of it has any connection to computing. More broadly, I think many computing people are too uncritical about the relevance of mathematics like AST to their discipline. They are very likely to find themselves disappointed.

yakubin 5y ago

> Pure mathematicians don't use computers or even think of them in their work, for the most part. That's not true. Many pure mathematicians use programs such as Wolfram Mathematica and Macaulay2 in their work. (Source: I studied maths and I know a bunch of them personally.)

ogogmad 5y ago
Agreed. The OP's assertion is questionable. I don't know how good of a mathematician I am, but I've certainly used computers in all sorts of ways: CAS, plots, numerical experiments, wikis/blogs/QA sites... You use whatever you can. Proof assistants are having a bit of a breakthrough as well, while previously they were associated with "inelegant" proofs or non-mainstream stuff for mathematicians. Mandelbrot talked about an anti-computer snobbery that permeated mathematical culture in university mathematics departments in the '70s, and how he overcame it and produced the famous Mandelbrot set.

sixbrx 5y ago

Might want to read the "Math and Computers Join Forces" near the end. Includes a use of interactive theorem prover Lean (functional language with a dependent type system) and some other stuff. Very much CS meets math.

wittycardio 5y ago

Theoretical Computer science is math

ogogmad 5y ago
The word "math" means different things to different people. It makes discussing the relevance (or not) of mathematics to computing difficult.

liups 5y ago

> pure math (topology and countability) and computer science have almost no overlap in the short term. This is an unexpected opinion. What do you mean by this? I would argue the opposite. Look at Formal Verification[0]. Here's a great video about a popular formal verfication proof assitant: https://www.youtube.com/watch?v=Dp-mQ3HxgDE https://www.youtube.com/watch?v=Dp-mQ3HxgDE A quote from the mathematician in the video expressing enthusiasm for using computers for mathematics: "All I want to do... I don't want to do mathematics on pen and paper anymore, because I don't trust it, and I don't trust other people that use it; which is everyone." (in case people only read this quote, instead of watching the lecture, the tone is tongue-in-cheek) Formal Verification would seem a literal intersection of pure math (formal proofs[1]) and computer science (formal specification[2]). Of note, one of the popular underlying foundations of an approach to formal verification is Homotopy Type Theory(HoTT)[3][4] which is an asserted effort to show the relationship between type theory and, specifically, topology (homotopy[5]). [0] https://en.wikipedia.org/wiki/Formal_verification https://en.wikipedia.org/wiki/Formal_verification : fancy word for 'computer verified mathematical proofs' [1] https://en.wikipedia.org/wiki/Formal_proof https://en.wikipedia.org/wiki/Formal_proof : fancy word for 'proof' [2] https://en.wikipedia.org/wiki/Formal_specification https://en.wikipedia.org/wiki/Formal_specification : fancy word for 'rules for an algo that checks a proof' [3] https://en.wikipedia.org/wiki/Homotopy_type_theory https://en.wikipedia.org/wiki/Homotopy_type_theory [4] https://homotopytypetheory.org/book/ https://homotopytypetheory.org/book/ : a great read, even if you are a novice, or prefer other formal verification foundations [5] https://en.wikipedia.org/wiki/Homotopy_theory https://en.wikipedia.org/wiki/Homotopy_theory : "It originated as a topic in algebraic topology"