←back to thread

Everyone is capable of, and can benefit from, mathematical thinking

(www.quantamagazine.org)
669 points sonabinu | 9 comments | 21 Nov 24 01:45 UTC | HN request time: 0.001s | source | bottom
Show context
penguin_booze ◴[21 Nov 24 12:56 UTC] No.42203880[source]▶
To my mind, the premature formalization of the math is the principal contributor to gas lighting and alienation of people from maths. The reduction of concepts to symbols and manipulation thereof, is an afterthought. It's misguided for them to be introduced to people right at the outset.

People need to speak in plain English [0]. To some mathematicians' assertion that English is not precise enough, I say, take a hike. One need to walk before they can run.

Motivating examples need to precede mathematical methods; formulae and proofs ought to be reserved for the appendix, not page 1.

[0] I mean natural language

replies(9): >>42203947 #>>42203971 #>>42204913 #>>42205113 #>>42205211 #>>42205397 #>>42205805 #>>42206498 #>>42216421 #
1. llm_trw ◴[21 Nov 24 13:09 UTC] No.42203971[source]▶
Mathematics is the conversion of a large number of object languages in to a single meta language that lets us talk about all of them.

The sin of modern mathematics is that it's meta language is so ill define that you need towers of software to manipulate it without contradiction. Rewriting all of it into s-expressions with a term rewriting system for proofs under a sequent calculus is an excellent first step to making it accessible.

We do not need to go back to the 16th century when men were men, an numbers positive. If people want to look at what math talks about instead of how it talks about let them pick up stamp collecting.

replies(1): >>42216489 #
2. Tainnor ◴[22 Nov 24 19:02 UTC] No.42216489[source]▶
Weirdly enough, mathematicians have been manipulating expressions and writing proofs for centuries without (routinely) stumbling into contradictions all without the need of formal proof calculi or s-expressions.

I have nothing but admiration for projects like Lean and Coq and working in them can be a lot of fun (coupled with a lot of frustration when "obvious" things sometimes take an inordinate amount of time to prove), but Wiles' proof of FLT (the corrected version) was published in 1995. We're almost 30 years later and people are just now working on a formalisation which could take many years (https://leanprover-community.github.io/blog/posts/FLT-announ...). Mathematicians can't afford to be waiting for proof systems to catch up, at least not right now.

replies(1): >>42217680 #
3. llm_trw ◴[22 Nov 24 21:53 UTC] No.42217680[source]▶
It wasn't until the 1930s that people realised second order logic with arithmetic will always lead to contradictions without guardrails. Before then all mathematics was done in the object language of whatever the field in question was and only translated to the meta language for succinctness after the fact.

The magic of modern maths is that we can now work only with the meta language and get results free from contradiction. For this we absolutely need a modern notation to do the new type of maths since we are no longer grounded by the reality of the object language.

replies(1): >>42218147 #
4. Tainnor ◴[22 Nov 24 23:13 UTC] No.42218147{3}[source]▶
None of what you wrote is true.
replies(1): >>42218157 #
5. llm_trw ◴[22 Nov 24 23:15 UTC] No.42218157{4}[source]▶
Feel free to explain why.
replies(1): >>42218245 #
6. Tainnor ◴[22 Nov 24 23:36 UTC] No.42218245{5}[source]▶
Your very first sentence is simply wrong, I don't know what more there is to say other than that you clearly don't understand what Gödel's results are about (hint: they're called "incompleteness theorems", not "contradiction theorems"). Maybe read a textbook? I could recommend several good ones.

The other sentences basically fall in the category of "not even wrong", i.e. basically nonsensical.

replies(1): >>42218327 #
7. llm_trw ◴[22 Nov 24 23:53 UTC] No.42218327{6}[source]▶
Godel starts by the assumption that the system is free from contradictions which makes his papers largely irrelevant here.

Again, feel free to explain how you can have a second order logical system without axiomatic limitations that doesn't contain contradictions.

Hell, go by the more popular version of first order logic + set theory if you're more comfortable with that.

replies(1): >>42218621 #
8. Tainnor ◴[23 Nov 24 01:19 UTC] No.42218621{7}[source]▶
Nobody has found a contradiction in (first or second order) ZFC in over a hundred years. You're out of your depth.
replies(1): >>42218711 #
9. llm_trw ◴[23 Nov 24 01:59 UTC] No.42218711{8}[source]▶
>Nobody has found a contradiction in (first or second order) ZFC in over a hundred years.

Yes, which is exactly why we have guardrails like ZFC in place. We got all sorts of exciting results without them. We of course have to keep adding axioms to ZFC - or replacing them all together - because there is a lot of math out there which is outside it's purview.

>You're out of your depth.

You're being incredibly abrasive for no reason.