ℝolliℵg M∀th Thr∑a∂

^^ 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/

flopson,
1) Partition Z into two countable subsets, say X and Y. For example, evens and odds. Creating a pairing between elements of the sets, then define

f: x |->  y
   y |-> -x

Haven't looked at 2 yet.

nice B-)

Believe 2a is n C n/2 for n even, zero for n odd.

hell ya

Darnit, you made those both look easy...

idgi

here's the problem i'm working on right now. you have a circle of radius R centered at the origin. you have a horizontal line y=b. find the center and radius of a circle that is tangent to the line at some arbitrary point (a,b) and tangent to the larger circle anywhere. help.

The way Clones of Baron F. polished off 1 and 2a makes me want to take a crack at 2b. I have a feeling that is a quixotic urge though, and one that will soon pass. Even if I drop the constraint that we end on zero dollars and just try to think of how many sequences never go negative, my brain still hurts.

For the circle one, it seems like you have 3 cases: R < b, R > b, and R = b. R = b is the easy case, I guess, because the 2nd circle will be tangent to the line and the circle for any 2nd circle with center (0, c) and radius |b - c| (except for c=0, because that would give you the first circle). Too tired to take a crack at the harder cases right now.

Thought I made some headway on 2b, but hasn't coagulated yet.

Looks something like 2^(n/2 -1) plus some lower order terms, for n even of course. Aargh.

Knew I shouldn't have changed my lucky screenname

flopson, why u braek weekend?

Okay I got far enough along on this that I am willing to either
1) Ponder it a little longer or
2) Read you official solution

k ill post solutions to both when i'm not on my phone

k thx.

One approach I seem to see

2^(n/2 -1) + n/2 C 4 + (n/2 C 6 ) * 3 + ...

can you explain

Sketch:

Let f(n) be the number of such paths for a given n.

For any n/2, always have solution +1 -1 + 1 -1 +1 -1 ....

One can also group the +1 -1s into pairs. In fact for any even k < n/2 one can choose choose a subset of k of the pairs and regroup into pairs of +1s and -1s and rearrange these groups so as to be solutions for k for the same problem ( you can divide by 2 or restate problem slightly ) This gives n/2 C k f(k) solutions.

General recursive formula is then
f(n) = n/2 C 0 * f(0) + n/2 C 2 * f(0) + ...

(continued in the next post)

Sorry, typo
f(n) = n/2 C 0 * f(0) + n/2 C 2 * f(2) + 2/2 C 4 * f(4)...

(continued in next post)

Examples

For n = 0 we say f(0) =1 (have to think about this)

For n =2 we have one path, namely +1 -1

For n= 4 we have +1 -1 + 1 - 1 or performing the "double up operation" +1 +1 -1 -1 so two paths.

Checking, f(4) ?= 2 C 0 * 1 + 2 C 2 * 1 = 2 check

(continuing)

f(6) = 3 C 0 * f(0) + 3 C 2 * f(2) = 1 + 3 *1 =4
f(8) = 4 C 0 * f(0) + 4 C 2 * f(2) + 4 C 4 * f(4) = 1 + 6 + 2 = 9

(cont..)

So was looking like powers of two until that last one. Now we observe that

m C 0 + m C 2 + m C 4 + ... = 2 ^(m-1)

which gives the leading term of my answer.

Why is the above identity true? Way I just saw it was to take

(1+1)^m + (1-1)^m = 2^m, see that alternating terms of the expansion cancel, and divide.

This is where I ran out gas for now.

Sorry, typo
f(n) = n/2 C 0 * f(0) + n/2 C 2 * f(2) + 2/2 C 4 * f(4)...

Typo^2 This should have been:
f(n) = n/2 C 0 * f(0) + n/2 C 2 * f(2) + 2/2 C 4 * f(4)...

At this point I don't know if I should keep studying/manipulating this formula until I get a simpler formula, or see if I made an error in deriving it, or try a different approach altogether.

Think I did indeed make an error and overlooked some cases and undercounted. Will ponder a while longer.

Still tinkering can't quite get the precise adjustment to my lower bound. Sorry to break thread.

Okay, now think the recursion formula is
f(n) = 2 f(n-2) + f (n-4) , n even

Aargh, still missing a few

Re-reading the circle question, I think I misunderstood it. The arbitrary point (a, b) must be given, otherwise it's too easy. I should have been suspicious that I made some headway on it so quickly.

Gave up and looked up this morning. Interesting. Hopefully can read more carefully tonight.

this thread is hard to find

anyway, first bunch of results for the 'mustn't go below zero, must end at zero' question
// 2 = 1
// 4 = 2
// 6 = 5
// 8 = 14
// 10 = 42
// 12 = 132
// 14 = 429
// 16 = 1430
// 18 = 4862

it's like a map

     /\
    /\/\
   /\/\/\
  /\/\/\/\
 /\/\/\/\/\
A   -t->   B

how many routes from A to B without backtracking?

f(n+1) = f(n) * (2 + (2(n - 1) / (n + 2))

which probably resolves down a lot

(oh, i've numbered those 1 - n where they should be 2 - 2n as only the even numbers work)

and f(1) = 1

scale factors between values are
2 + (0 / 3)
2 + (2 / 4)
2 + (4 / 5)
2 + (6 / 6)
2 + (8 / 7)
2 + (10 / 8)
2 + (12 / 9)
2 + (14 / 10)
etc