top | item 29721063

The year in math and computer science

156 points| ghosthamlet | 4 years ago |quantamagazine.org

9 comments

order

redis_mlc|4 years ago

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.

yakubin|4 years 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.)

liups|4 years 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

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"

jhgb|4 years 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?

wittycardio|4 years ago

Theoretical Computer science is math

sixbrx|4 years 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.