Your professor is in the "post-rigorous" stage of his or her life.

At any rate, it doesn't matter: metaphor was always the foremost source of mathematics, and as far as geometric topologists are concerned, those metaphors may as well be pictures.

If this weren't the case, then human's wouldn't be necessary, since all mathematics could have been proven by brute force using a computer, straight from the precise problem statements in terms of their definitions. Whereas in reality, "creativity" sill plays a role, since humans very often solve problems by formulating new ones, or restating them in ways that make use of subtle patterns, rather than taking a direct route.

But it's starting to happen anway, and Doron Zeilberger is (controversially) cheering this trend on and extrapolating far (or not so far?) into the future.

For example, if the kind of picture that Danny draws in the second link were a prohibited activity in mathematics, then complex numbers or even negative numbers would never have been allowed to be invented.

Foremost mathematics is an art, so I would never apologize for drawing an impressionistic picture to get a point across! That said, following Tao, undergraduates need the rigorous part, so that they don't use their intuition to sabotage themselves.

When I sat in on geometric topology for a few lectures, the professor started out by defining operations on pictures using definitions from algebraic topology: she discussed things like homotopy and isotopy to define the rules of what was happening.

In prior years, though, a far more experienced topologist had taught the course. I am told that in this course, for the most part, only the pictures were taught.

I remember reading that when Feynman introduced his diagrams, a certain number of people were very upset: they had spent years in graduate school learning to calculate integrals that undergraduates would now be able to find the answer to simply by following the rules of a stupid little diagram.

tl;dr: proofs : calculation :: mathematics : physics

(neither are the point)

I really need to read this book to make sense of the relation between proofs and programs (hey, look who translated it).

If the point of proofs in classical mathematics is to catch bugs in theorems, wouldn't that make the logic used to formulate these proofs analogous to types as used by software engineers, which are billed as a way to catch bugs in programs? But I'm not so sure that's the kind of thing the Curry-Howard correspondence is explicitly about.

That's fine. I can be the Koobie, part time



Damn, I'm nowhere in good enough shape for that. I'm at the phase still where it's hard to run 3 continuous miles. It doesn't help that where I live is super hilly, which makes running like exponentially harder, but still, I'm not fit for 13 miles.

Someday though. Someday.

How is Reid more Koobie than me? He's polite and intelligent rather than overly obsessive and overly sensitive like me.

You already failed at being Koobie, Ried. If you were Koobie, you would have responded to saberopus by calling him a Koobie.

I ran this last one today in 2 hours and 15 seconds. Not going to lie, I feel like a beast! Pretty dope that it was in Jerusalem, too. Which also means it was pretty hilly. But yeah, it's taken months of training 5x a week to get here.

Speaking of Koobie, has anyone ever played kubb?

If we combine your stream-of-consciousness twenty-posts-in-a-row compulsion with Reid's, like, one instance of micro-blogging I decided to comment on, then why, that'd like, that'd leave us with, somethin

At least your sensitivity leads to you excessively apologizing for your posts instead of getting defensive and mean. That seems more common or likely, really.

I have a tendency to get mean and hostile when people challenge my views too hard, it's a real problem.

I instigate conflict unnecessarily

I get into conversations at inappropriate times and then leave suddenly without contributing anything of value :saddowns:

I am a low effort ****post based lifeform

high effort bull**** post based life form standing by

:justpost:

I've always found the 'class clown' role to be convenient, making it easy to say whatever I want and then just apologize (sincerely) if I take something silly too far.

But doesn't my sincere apologizing just make me a beta male? The true alpha will never apologize for his mistakes!

https://news.ycombinator.com/item?id=16557784

Why are people here talking about ML algorithms unexpectedly and randomly 'hallucinating' things like Alexa commands out of nowhere? Does this mean that if Trump sells our ICBM arsenal to a Amazon, that Alexa may 'hallucinate' a cold war?

And I thought that early launch warning satellites which mistook reflections off of clouds were frightening enough. But this incident would have resulted in certain doom if the launch system were completely automated with a Bash script in the cloud!

Is it really a good idea to give the machines control of things that we don't want to do before we even can be sure that they 'know' what they are doing? I'm scare

https://getyarn.io/yarn-clip/2c93361f-486a-4940-acfb-51fa92c72539

- how I often feel about machine learning

It's going to be very, very long before we have any computer systems which can reliably and consistently interact with human symbols. Possibly even impossible.

Computers are just fundamentally different objects that work on physically different principles from brains. Trying to model one in the other seems like it would take ages of refinement and tweaking, and I'm not really sure what the benefits are.

Also yeah they shouldn't be used in sensitive areas. Pretty much anything that could get people hurt should be devoid of ML.

Your honor, my client.java

Fixed.

ML is a perfectly legitimate way of computing answers. Even in situations like healthcare diagnoses, ML is proven superior to human doctors. Just don’t let the computer make its decisions by itself and you’re fine.

It’s like


Computers are superhuman at chess now, right? Even an old flip phone can beat the best human chess players. But a human working with a computer is far better still. Humans are bad at crunching data but we’re very good at... something. Something that I don’t think we’ve ever successfully described, let alone quantified. Computers and humans are at our best when we are working together.

Humans are good at being social and lazy. By comparison, computers are basically autistic workaholics.

Hopefully our laziness doesn't lead us to hand the keys over to our new idiot savant overlords.

i think what you're looking for is internet porn

In differential topology we discussed a few proofs that justify the intuitive "picture-drawing" things you see in topology. It's all good to go post-rigor, but only after you have the solid intuition for what's a "right move" in topology.

But mathematics is never rigorous. It's just a matter of how rigorous you want your proof to be. Some people go more formal than others, but nobody is fully formal or fully informal. IDK what a formal proof would even look like, because you'd have to cite a huge amount of theorems that reference ZF axioms so frequently it would be a huge mess. We always take a bunch of stuff for granted.

For sure, we use ML to come up with predictions, then doctors audit the findings. That's a model where ML works fine.

I was thinking a bit recently about comments about math only wanting to rely on self-consistency, and after reflection of the facts, the more I'm convinced that all sciences have drifted towards the frame of being merely "self-consistent", and have abandoned the idea of ever creating an intuitive understanding of the universe. I actually checked out a bit of the book Principles of Quantum Mechanics by Paul Dirac, and he more or less says this directly.

Here he outlines what quantum mechanics seeks to achieve, two parts:



And on intuitively understanding physics:



And the text itself is littered with the phrase:









I find it increasingly true that the only significant difference between physics and mathematics is that physics portends to create theories that conform to experimental results. In fact, Newton's works were rejected largely on similar principle: he created consistent systems that necessitated theories of gravity which were not grounded or easy to comprehend. And he was rejected by many contemporaries on grounds that his ideas involved occult mysticism, basically forced on the level of scholastic sympathies and antipathies and were not grounded in intuition.

So, the idea that mathematics is "empty formalism" whereas physics is "useful mathematics" is a weak one. In fact, I'd even argue that physics has only made gains in the sense that it has become more like mathematics, concerning itself more with self-consistency and formalism, rather than a theory which portends to explain the machinations of reality itself.

Nobody really cares much about axiomatic set theory as far as I know. Maybe in measure theory it matters. But it's ridiculous to say that "no mathematics is rigorous". I guess you're referring to something about Gödel's incompleteness theorem, but there are plenty of perfectly clear theorems in (say) combinatorics that couldn't be made any less ambiguous if you tried. Unless you want to argue that those things aren't "real" mathematics because they don't require pathological non-sense to be precisely interpreted!

What Terry Tao means by "post rigorous" is that the mathematician presumes herself or himself to be fully capable of writing a proof in the level of detail expected, but doesn't, because:

1. s/he is virtually certain that the statement is true, and
2. has better things to do.

This post is interesting to me and seems to talk about a lot of things that I agree with, but: where did you ever hear this? Certainly not from me.

People don't really write formal proofs. For instance, it has to be shown that a function which is not injective is not bijective. Any time in a theorem you use that, you don't cite it, you presume it. A formal proof would have to cite such things.

That's what I mean when I say "no mathematics is rigorous". Most proofs operate on "a person with enough understanding can see how this could possibly be written as a formal proof under some axioms". That we can see that it's implicitly valid is enough, we don't verify very far.

It's not that different from physics, really, where they don't attempt to justify their math all of the way down.



I'm not sure I liked that thing about pathological nonsense, because 1) it's finitist nonsense and 2) it fails to understand what humans do.

Consider:



Every single physical theory we have is a practical necessity. Things like Niels Bohr's theory of the atom is not very different structurally from the "Hilbert-Cantor Paradise", it fails as a theory, and nothing else we have quite works to describe chemical bonds. The only difference is because we pretend Niels Bohr theory gets at something "real", it must be a "better theory", despite it being an inadequate model. So criticizing the existence of infinite sets based on a dislike of weird consequences is, in my mind, not far from criticizing the discoveries of nearly all of the more important physics. Everything we ever create that's of any value depends on weird, counter-intuitive, and more importantly, "wrong" assumptions.



Exactly, yeah, formal math in that sense doesn't exist. We presume the existence of formal proofs and move on.

It's just a point of rhetoric, don't read into it too deeply.

http://sites.math.rutgers.edu/~zeilberg/fb68.html

Also, lol at this reply to that finitist rant.

When I took undergraduate physics, my professor HEAVILY criticized the Niels Bohr model in quantum mechanics. We spent about five minutes on it just to make fun of how bad it was. It is a chapter in history.

Doron Zeilberger's point (and I will be the first to admit that he is often over the top / needlessly provocative in making his points) is that axiomatic set theory occupies a similar position today in mathematics: a mostly defunct, historical relic, that has been made obsolete by computers (for calculation), as well as category theory (for ergonomics).

I feel that Dana Scott's (excellent) reply both moderates and informs Zeilberger's point: Scott merely points out that such pathologies have been present in axiomatic set theory for a long time now!

I do find your analogy between models in physics and mathematical theories to be quite apt.

However, physics has experiment to act as final arbiter of the quality of a physical model. What the heck is the final arbiter of an axiom system in mathematics? Intuition? Consistency? Axiomatic set theory smells like a bad mixture of both of those things (with intuition playing a larger role perhaps in the early days of set theory, such as Hilbert's "Platonist" belief in infinity mentioned by Zeilberger).

That all said, from what I understand, the independence proofs of Paul Cohen, which introduced the method of forcing, are beautiful and interesting results unto themselves, which opened up entirely new avenues of mathematics within set theory, and perhaps proved to be more interesting than some of the things that the original set theorists thought were so important. (Of course, this is all rather heady stuff and I don't understand any of it, so don't take my word for it.)

Of course, Zeilberger even likes it. But he thinks it's all just "combinatorics" in the end, and doesn't give a hoot about its interpretation.