ℝolliℵg M∀th Thr∑a∂

Mega thumbs up for Courant and Robbins, and for Gowers. Not for Kline or Stewart.

Wazzabout Geometry and the Imagination, Hilbert and Cohn-Vossen?

obv a classic

i enjoyed both kline and stewart, though i ultimately felt stewart lacked depth. kline was a little dry, i guess

They're not super well-informed, that's all.

You might enjoy Plato's Ghost?

damn, too late for a PIDMAS joke

what do you mean, euler?

"plato's ghost" sounds great!

Wow, lot's of rave reviews for Plato's Ghost on Amazon, including yours.

I just mean that Kline esp didn't know his stuff very well.

Plato's Ghost is fun! but haha a uh friend of mine is quoted about it by the publisher on the Amazon page. positive quote

xp eek

Hm. NYPL has Plato' Ghost but it is completely different book.

Plato' Ghost must haunt me now

my kids thought it was a scary book when they were littler. we had to hide it

that VSI is kind of a miracle. every other VSI (including the cosmology one) is shoddy or cursory or biased or otherwise weird. but that is afaict an effective, readable and serious introduction to professional higher mathematics. and it's like 50 pages. i should definitely take a look at his princeton companion.

the more traditional NPR pop maths book i liked most recently (i.e. published in the last 10 years) was zero: biography of a dangerous idea. good book.

Some are better than others. The one on Galileo has a strange angle to push, one on Newton is pretty good I think.

Maybe you are near a library that has it?

― Lemmy Cauchemar (James Redd and the Blecchs), Saturday, May 16, 2015 11:41 AM (3 hours ago) Bookmark Flag Post Permalink

work for UW now so I can abuse my library privileges for it I guess.

Newton one was written by head of the Newton Project.

Author of Galileo book was no slouch either, although now I can see the book was not written to be a short course.

Of the little pop math I've read recently, I liked Ekeland's "Mathematics and the Unexpected".

I just read the VSI on antisemitism and it was very weird, more a history of the Holocaust than anything, but it had a couple of outstanding chapters that made it worthwhile. gonna read the german philosophy volume next.

that was just about the VSI series. obligatory math content: Mathematics Under the Nazis by Sanford Segal is fascinating

the german philosophy one is just a reprint of an old scruton book iirc, would give it a pass

was looking at one by Andrew Bowie ?

who I don't know, but I want some guidance on where to start with german idealism re. the rise of German anti-semitism in particular

oh, it seems they've replaced the old one i read then

Have always seen those Morris Kline books about, never read one. This other guy Carl B. Boyer looks like he might be good though

RIP John Nash.

at least they went together, that's kind of cool i guess

not a nice way to go though

apparently gromov said that john nash's work in differential geometry was infinitely more important than the game theory stuff

got some great riddles for y'all

(1) name a function f: Z->Z such that f(f(x)) = -x for all x in Z. note that f(x) = i*x is not an answer because it doesn't map Z to Z. (hint: there are infinitely many solutions)

(2.a) (easy) consider a game where you flip coins. i give you a dollar when it comes up heads and take away a dollar when it comes up tails. for fixed n, how many sequences are there such that you end the game with zero dollars?
(2.b) (hard) how many sequences are there such that you end with zero dollars, but never have negative dollars?
(2.c) (hard) call a peak the largest number of dollars accumulated over the course of the game. for example, if n=4 and you flip HHTT, the peak is two. if you flip HTHT, the peak is 1, attained twice. prove that exactly half of all sequences such that you end with zero dollars attain their peak exactly once.

you should all be able to figure out (1) and (2.a). i'll let you torture yourselves for a week or so then post the solutions to (2.b) and (2.c)

apparently gromov said that john nash's work in differential geometry was infinitely more important than the game theory stuff

everybody on earth says this, not just gromov

His work on complexity would’ve likely been even more important than his Riemannian manifold or game theoretic work if it were declassified in a timely manner. But I’m biased, obviously.

Thanks for the problems flopson. I’ll play with these over the weekend.

can someone tell me how big a deal this actually is? There was like a brief period four years ago where I was maybe almost trying to get some clue about what the scope and aim of studying foundations is and also a brief tutorial in formal verification and so like what is happening here

https://www.quantamagazine.org/20150519-will-computers-redefine-the-roots-of-math/

^^ that's related to my field of study and i tend to think it is a very big deal, though the article is only talking about one recent development.

the question is sort of vague so i'm not sure how exactly to reply tho. the main thing, i think, is that lots of strands that intersect in homotopy type theory all get grouped together but need not be. e.g. you can look at proof theory without taking a foundational stance, and computer verification likewise. and there are a few ways for the two to intersect, of which type theory is only one. and there are people who study "foundations" in a more classic set-theoretic sense and their work is not designed to relate to automated verification or the logical element of proof-theory at all, and also people who study it in a philosophical sense and their work is only sometimes considered "mathematical" in a direct sense.

the intersection that the article writes about is an interesting one though, not least because you have a few folks coming from a very abstract tradition and not interested traditionally in computer assisted proofs now both getting interested and also making important contributions.

but on the whole i think the technology for these things to find widespread use is still a ways off -- you can formalize way more than people imagined, but it is a tremendous amount of work to do so. (two large recent successes in this area: http://www.msr-inria.fr/news/the-formalization-of-the-odd-order-theorem-has-been-completed-the-20-septembre-2012/ and https://code.google.com/p/flyspeck/)

the field of homotopy type theory is independently interesting too, but there's a legit question at what point it'll start bringing "big" useful contributions to more mainstream mathematical problems.

i also think a younger generation of people who have been growing up with programming and computers are going to be way more receptive to integrating this stuff in their everyday work. people who spent their careers working with other tools aren't for the most part going to take a headlong leap into something new (people like voevodsky and hales are significant, important, exceptions).

idk i'm just rambling now -- if you have any more specific ways of framing questions i'd be happy to answer in more depth

I don't think it's a particularly big deal; as Michael Harris insinuates in the article, most mathematicians don't care about "foundations" in the sense of ensuring the rigor of mathematical proof. They're happy enough with the current standards of rigor. That's normal in the history of mathematics: the early twentieth century "crisis of foundations" originating with the paradoxes makes sense, in retrospect, as a reflection of the time, as a reaction to mathematical modernity. 100 years later, it doesn't seem so pressing: we've come to grips with modernity.

it's def true that there's a lot of money in proof checking now, b/c software companies (esp microsoft) fund this research in the hopes that it'll contribute to better tools for software verification. as the actors in these projects are well aware.

there's a big distinction to draw between verification and foundations with a capital F though. and between rigor with a lower and uppercase R. So one question is "can you formalize this down to the bone" and another one is "are you sure that all the times in this proof you solved a system of linear equations you didn't miss a step" and the latter are where it tends to get more interesting. to me the hales story is the most compelling in this regard.

the other thing is there's a distinction between "will most mathematicians today start using proof assistants" (clearly, no) and "are the mathematics of proof assistants surprisingly deep and rich" (at this point, yes -- and this will lead to interesting work including probably to a renewed interest in how classical results fracture in an intuitionist context) and "does the syntax and style of homotopy type theory yield insights even when working in an informal setting (i.e. at a chalkboard with no computer in sight)" (and here, the answer is probably 'depends on your taste', but i think over time it will gain increasingly widespread use because of its convenience and universality).

and of course there's also "will this transform software development in some sense" (which also would be a big deal) -- and the answer is "if so, any direct impact will be a loooong way off."

(really weird to be discussing this on ilx)

and also there's "does the HoTT approach have insight to bring to bear on the study of infinity-groupoids, infinity-categories, and infinity-toposes" -- this is unclear, but potentially the case and relates to the "even in an informal setting" thing i mentioned above.

I'll ask some better questions a bit later but thank you so far! Weird math is well beyond my skillet but I find it tantalizing. Kind of like how I felt about computational complexity when I was 17.

OK so I guess to back up a bit and ask a better question, what is it about categories and types that make them attractive to this batch of people as an axiomatic basis for…whatever, higher math in general I guess, vs. ZFC? The article of course mentions the foundations crisis and Russell's paradox, but it seems like most of math just went on cheerfully generating good results with sets, and the non-infinitarian people were cheerfully doing combinatorics in Matlab etc.

there's a big distinction to draw between verification and foundations with a capital F though. and between rigor with a lower and uppercase R. So one question is "can you formalize this down to the bone" and another one is "are you sure that all the times in this proof you solved a system of linear equations you didn't miss a step" and the latter are where it tends to get more interesting. to me the hales story is the most compelling in this regard.

what's the difference between "formalizing down to the bone" and checking that you didn't miss a step? isn't the ONLY point of the former, the latter? for instance set theory, I guess an instance of what you call "formalizing down to the bone", was created to ensure gapless reasoning concerning the infinite.

I somehow don't find myself attracted to the idea of foundations and proof verification at all, but the little I know about homotopy type theory seems fundamentally interesting. It just smells right.

(as a self-xp obviously type theory has been influential in the proglang/CS "theory B" world but dabbling in Haskell aside I've never cared that much about it)

what's the difference between "formalizing down to the bone" and checking that you didn't miss a step? isn't the ONLY point of the former, the latter? for instance set theory, I guess an instance of what you call "formalizing down to the bone", was created to ensure gapless reasoning concerning the infinite.

― droit au butt (Euler), Wednesday, June 10, 2015 12:00 PM Bookmark Flag Post Permalink

well there's a purely philosophical point to the former, in that it gives you some notion of "truth", and you usually argue about "what the right bones are" -- i.e. should you "really" have excluded middle or choice or continuum hypothesis or any of the funny weaker inbetween things or variants -- less limited partial omniscience, wllpo, negation of CH, etc. are your "base objects" really sets or categories or etc.

but in the latter you can start of think from "top down" and say "every proof has a bunch of steps, some omitted, some not. proofs may be wrong because the omitted steps may not be as obviously correct as we think, or they may be wrong because a step we took was actually wrong." for the latter, imagine that you're calculating something and forget to account for the case when there's a zero, and we accidentally divide by that "might be zero" thing, and it busts things up. or even more obviously, maybe it depends on being split into some set of checkable cases, which in turn depends on certain things summing correctly and you just add the numbers wrong.

So you can take your proof and admit whatever assumptions you want to "get off the ground" and admit whatever higher level theorems you want, but you still can use verification to make sure that you're not using those higher level things right.

So you can just admit something like the entire theory of groups and basic results on them or something, rather than reducing all that to set theory, and a proof verification system still helps you say "given all these assumptions, am i making sure to work with them in the right way" etc.

OK so I guess to back up a bit and ask a better question, what is it about categories and types that make them attractive to this batch of people as an axiomatic basis for…whatever, higher math in general I guess, vs. ZFC? The article of course mentions the foundations crisis and Russell's paradox, but it seems like most of math just went on cheerfully generating good results with sets, and the non-infinitarian people were cheerfully doing combinatorics in Matlab etc.

― jennifer islam (silby), Wednesday, June 10, 2015 11:57 AM Bookmark Flag Post Permalink

so ZFC is never just ZFC. that just gives you axioms. you then need to associate those axioms to a logical system that lets you put them together to get new results. type theory as a development of logic is a way of giving a very uniform syntax to that logical system, which is both, if done right, friendly to people and how we like to look at formulae, and also friendly to machines and the ways in which they can be good at checking the correctness of formulae.

there's a huge world of proof systems, and actually the most popular ones aren't rooted in type theory, but do have some sort of set-theoretic background -- higher order logic + the theory of sets or something. type theory just has a number of properties that make it especially simple to work with / reason about.

(categories don't really enter into this side of it at all, tbh).

one element of type-theoretic provers is that they're especially suited to "constructive" proofs -- i.e. we read off our propositions as "types associated to functions" and then our proofs can be read as "implementations of those functions" and so we carry around instructions for how to actually "execute" proofs. This isn't always possible, but it is very handy. For example, one might have a theorem that for a particular setup, some unique minimal element exists. Then some other proof might make use of that element, and require actually having that particular element, to calculate on it. So the first proof, though it appeared to be just an existence proof, actually had constructive content which it was necessary to make use of elsewhere, and if you set things up right, then you can rely on that having been taken care of for you (here's a good talk on the topic: https://video.ias.edu/members/1213/0318-AndrejBauer).

The theory of types is also suited to introducing new "mathematical objects" as they say "synthetically" -- so if you start with ZFC and want the natural numbers you have to "pick" that your naturals are e.g. the empty set, the set containing only the empty set, and soforth on up. If you're in a type theoretic setting you say your naturals are defined up to unique isomorphism _directly_ (and the univalence principle in HoTT makes this even stronger). So this this avoids the awkward step (computationally) of encoding lots of things that don't feel at all like sets in structures of sets (even though this can of course be done in theory if you really wanted to).

In HoTT this becomes even more powerful because of the natural correspondence between the structure of the identity (or "equality" if you prefer) type, and "homotopy paths" so that rather than build up to homotopy theory via a bunch of successive encodings that go down to raw sets, you have these relatively sophisticated mathematical objects built right in.

(just to add to the point on categories: while there are some arguments made by commutative diagrams in the HoTT book, you could read through nearly all of it without having been exposed to the idea of category theory, and be able to follow what's happening -- in this particular context they're not considered as "core" to anything in particular [though the work on "models of HoTT" to give it semantics is very much in a categorical vein, I should add])

sorry, not sure if anything i wrote is comprehensible. its hard for me to judge what is "basic" or not in this area

i don't really follow the current conversation (though it sounds very interesting) but my friend recently read kleene introduction to meta-mathematics and parlayed the general sweep of it to me, got my curiosity juiced up on foundations.

http://i.imgur.com/awltf.gif

anyone wanna attempt answers to my riddles? 1 and 2a should be easy

http://news.nationalgeographic.com/2015/06/150621-mathematics-cooking-food-education-ngbooktalk/