The year in math and computer science(quantamagazine.org) |
The year in math and computer science(quantamagazine.org) |
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.
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.)
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.
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
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 : fancy word for 'computer verified mathematical proofs'
[1] https://en.wikipedia.org/wiki/Formal_proof : fancy word for 'proof'
[2] 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
[4] 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 : "It originated as a topic in algebraic topology"
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?
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.