Voevodsky has an Erdos number of 4. I don't see one for Michael Harris. So Voevodsky is obviously right.
Your code should be outputting a proof in a formal logical system, which has simple rules whose application is easy to verify. In practice I think you'd output a proof in Coq or whatever (I studied using TPS but it's clearly not the state of the art).
To make mathematicians happy, we'd want to have some sort of de-abstraction: a compiler that could take programs that look more or less like normal proofs and generates from them logically verifiable proofs in a formal system. I don't know if it's possible to create such a language for practical usage, since mathematicians like to hand-wave around the annoying but not deep bits. That could be ameliorated by building up libraries of standard definitions and proofs. There's probably been a lot of work on this already.
Obviously I didn't read the article, and a distinction can be made between automated theorem proving and specifying proofs in a formal environment. There are all sorts of heuristics to prune the space of all possible well formed statements, but I don't remember any of the techniques and didn't study them long enough. I'm imagining more computer-assisted proofs, where the human provides major key-frames in the proof and the computer fills in the details.
I took a CS grad class on this stuff. It was really interesting. We used Agda instead of Coq, but I don't think that's a huge difference. There's still a ways to go before this will be usable for most mathematicians (needs to become as easy to use as Tikz for significant use and LaTeX for widespread use). I really learned a lot.
Speaking of the social aspect of proof checking, the ABC conjecture situation continues to be an embarassing mess. No errors but still people can't really read it. The author is pissed and telling people that they just need to spend 3 months going line by line, and not trying to skim for ideas.
I'm imagining more computer-assisted proofs, where the human provides major key-frames in the proof and the computer fills in the details.
There are some systems (like this) that do that for security proofs in cryptography. It works as long as the proof has a standard structure -- a sequence of "games" that are all shown to be equivalent, using only simple arithmetic and probability. I think it's about as smart as a 6th grader?
Writing a proof checker is considerably easier than writing a system where the computer actually generates the proofs and fills in all of the holes that humans would never bother to fill in. It's simple enough that there are classes that do it as a final project. A couple of years ago someone wrote a program to output the proof of the 4-color theorem in a form that proof checkers could check, and it was indeed a valid proof.
One thing I find striking is that areas where it's hard to apply intuition, people will routinely miss very short proofs. In the area of distributive groupoids, computers have solved open conjectures with proofs of 10 lines or so. In areas where people have very detailed intuition, they find proofs of 100s of pages that computers are a long way from finding.
5, is that the Mochizuki story? What a weird story. It's like something from The Baroque Cycle.
7: Yeah. You just have to believe the proof checker, which should be trivial if the proof is written in a formal system with the requisite properties. In the limit, this is actually hard--e.g., do we believe that the underlying operating system is well-behaved? Have intermediate layers (e.g. the actually pretty well specified Java) been shown to be trustworthy, both in specification and implementation?--but for the most part I think mathematicians who refuse to believe the four color theorem, etc. are just being jerks.
Here's Mochizuki's complaint: http://www.kurims.kyoto-u.ac.jp/~motizuki/IUTeich%20Verification%20Report%202013-12.pdf
-but for the most part I think mathematicians who refuse to believe the four color theorem, etc. are just being jerks.
No one doesn't believe it. They just don't think it's pretty.
First, math is completely consensus-based.
Well, I have no clue about the math or computer stuff. But socially constructed discourse and reality I know a tiny bit about.
Lacanian Discourse Analysis:Ain't nothin' but signfiers making new signifiers signifierizing all the way down to the giant turtles. No signifying, no signs, no signified.
And the most usual discourses, like the geometry perfessers or here, are about using the emptiness of communal language to reveal and adjust subject positions in a social structure
12: They're worried it will cry if they put it that way.
I'm unusual in that I really like the proof of the 4-color theorem, and think it's plenty pretty (especially in the form given in "An unavoidable set of D-reducible configurations"). From my perspective, the main flaw in the proof is the human part, not the computer part.
What I mean by that, is that the computer is basically doing two things each of which are beautiful mathematically, conceptually easy to understand, and entirely mechanical. First it can take a collection of "discharging rules" and produce a list of diagrams such that every planar graph contains one of the diagrams somewhere. Second, it can take a diagram and show that it can't appear in a minimal counterexample to the 4-color theorem. So the proof goes: start with a collection of discharging rules, have the computer produce the list of diagrams that must appear in any planar graph, and then have the computer check that none of these diagrams can appear in any minimal counterexample. Hence no counterexamples. The problematic step is where the discharging rules themselves come from. That part is an art and not a science. It's produced by people by trial-and-error guided by their intuition. You try one set of rules and see if the computer can prove the 4-color theorem, and if it can't you go back and fiddle with the rules. What I would like is a completely computer-produced proof, where that first step was also automated and there was no complicated human input.
12: I thought there were people that didn't accept the validity of hugely complex computer generated proofs, ones essentially too big to go over manually, but perhaps that's not longer true or I'm misremembering.
Wouldn't it just be easier to use five colors on a map? It probably doesn't cost much to use one more color and I bet it takes a great deal less fidgeting with the map.
Unless it's 1991 and you're working in CGA graphics.
The corresponding and weaker Five-Color Theorem is much easier to proof; it can be done in a lecture or two in an undergrad graph theory class.
I actually feel like UPETGI and Heebie should team up and write a math book for non-math people. 15 was extremely interesting and easy to understand. I mean, I get that it was easy to understand because it was just descriptive about concepts and didn't do any actual math, but, still. Compare to math Wikipedia, aka the zero comprehension zone.
Related to 19, I wonder what non-coders actually understand or get out of reading this (warning, egregiously long-form internet writing):
http://www.bloomberg.com/graphics/2015-paul-ford-what-is-code/
It's kind of perfect for me as someone in the relatively early stages of being a career-switcher without an engineering background, but experienced enough to get most of the jokes. I am not sure how helpful it would actually be to the person who is supposed to be the piece's central conceit: someone who must manage coders but does not code.
19: That's pretty much all math is (this may be controversial), just there's layers and layers and layers of definitions built off of each other. The motivation for those definitions--which are of course arbitrary, since mathematicians get to make up their own world--might only make sense if you know decades of development.
Add on top of that the specialists who write the most arcane Wikipedia math pages are so used to thinking about their own very constrained world, communicating only to people in their subfield or near neighbors, and it's a recipe for disaster.
the motivation for those definitions--which are of course arbitrary, since mathematicians get to make up their own world
Um
20 -- that looked interesting, though I only skimmed long enough to read the part where he claims that there are 11 million professional software developers on earth, plus another 7 million hobbyists. 18 million people! That's maybe 18-20x more than I would have guessed.
Have all finite groups been classified or whatever? As I understand it, that's a nonsurveyable proof generated by a team in many papers over decades.
I went to a lecture in about 1980 asking whether computer proofs, including of the four color theorem, should be accepted by the mathematics community.
Formalist in the streets, Platonist in the sheets.
Finite *simple* groups... Yes, that's a big mess. The short version is that they declared victory before things were really over (one of the last papers just never got finished), and that declaration of victory made the field no longer attractive to new people. My understanding is that all the holes are thought to be patched now, but there's a bit of a race against time to see whether a simplified understandable 2nd generation proof will be finished before everyone who understands the field dies.
It's like Game of Thrones, except I'd bet the people involved are older than Martin.
20: The length is fine. That fucking robot needs to die.
To correct the OP, while I did in fact like the graphics, I was mostly interested in the explanation of Homotopy Type Theory and its relationship to set theory, which I found nicely coherent.
I am pretty basic, though. Whazzaaaap
|| For the non-math inclined, it's a pretty interesting day for DC Circuit opinions. http://www.cadc.uscourts.gov/internet/opinions.nsf Military commissions, Whole Foods mistreating customers, 9 year old strike at an LA hotel, timber company standing to complain about restrictions on logging, mobile broadband. The Iranian spy case is under seal, though. |>
Actually, I quite like math. Applied math at least.
though I only skimmed long enough to read the part where he claims that there are 11 million professional software developers on earth, plus another 7 million hobbyists.
I am a bit surprised at the hobbyist number and am wondering whom it is including. If it includes people who write code as a tool for their job but whose primary responsibility is not delivering software (e.g., many scientists), then it feels totally reasonable.
The length is fine. That fucking robot needs to die.
I have to be believe it's a winking Clippy reference, not that that excuses it (some of the animations are nice, though).
The philosophical book on mathematics I like best is Kitcher's "The Nature of Mathematical Knowledge". Supports the consensus notion. Also, I am a maths cripple, but the discussion of the underpinnings is still interesting.
I think at one point I suggested to some philosophers of math arguing about what is and isn't a real proof that everything they were pointing out (and all the accompanying problems) seemed like exactly what you'd get if you were dealing with a functionally defined kind of thing, where membership is a matter of being good or bad in certain respects but without an obvious line between 'a really awful proof' and 'not a proof at all', which means that they're kind of the same thing as tools. They're understood generally in terms of what they do, and depending on their possession of the things that make them good at doing it (like, for hammers, handles long enough to act as functional levers, heads hard enough to knock in nails, generally durable enough to be used to strike things repeatedly, etc.) they fall into vague-ish categories like 'excellent hammer', 'fine hammer', 'hammer', 'crappy hammer', 'awful hammer', 'not a hammer at all at that point', but without any strict lines involved.
So proofs are for proving things to us so they're better proofs when they're elegant, when they reveal interesting things about the underlying structure of what's going on, when they display a new insight, when they're robust or reliable, that they're hard to be skeptical about, (etc.), and the less like those things they are the less of a proof they are.* If so then it's easy to talk about some kinds of computer proofs not really being real proofs (at the extreme hypotheticals level), or at least being really crappy proofs, and other kind of proofs being better proofs or more ideal proofs, and so on.
I couldn't tell if the reaction I got was "that's dumb enough that it's not worth pointing out why it's wrong" or "well ok it probably is but if that's true there's nothing useful about all this work we've done arguing about necessary and sufficient conditions so we're going to say it's an interesting idea and then make sure to forget we ever heard it." I'm not sure those are even different things, sometimes.
*Math gets a lot of prestige but from what I've seen of the higher level stuff it's as much a form of studio art that turned out to have weird but super useful results in some other area as it is a really important means of gaining knowledge about the world, like if it turned out that impressionist paintings of tulips could cure tuberculosis or something.
I suppose in fairness telling them that they sounded like a bunch of metalheads arguing about whether it's more important to be brutal or kvlt was unlikely to get a useful response. I didn't actually say it that way at the time but in retrospect I totally should have.
Ok, so not immediately recalling what the four color theorem is, I hit wikipedia. I had to convince myself that the obvious 'disproof' indeed doesn't really work, and then the theorem started to seem pretty straightforwardly true. (I.e., basically, what De Morgan said: four areas cannot all have boundaries with each other without at least one being completely 'inclosed'.)
I guess it's one of those things that seems tots obvs., but the actual proof is really hard?
(Apparently Kuratowski proved in 1930 that there are no complete planar graphs higher than K4 - which seems like it's basically the same idea. Am I hand waving something important there? Is the four color theorem stronger than that?)
(Wait. Nevermind. I guess all that really proves is you'd need more than the minimum 5 nodes. But maybe the hypothetical counterexample is some monstrously complicated constellation of umpteen node. So reducing the potential configurations down into something manageable is probably the hard part... Duh. Should have checked with the computer.)
I'm reaching back here, but if I remember from my undergraduate topology seminar, the proof of the Heawood conjecture due to Ringels and Young doesn't work in the case of the sphere and the plane because the Euler of the sphere is 2, and in the case χ = 2, their proof would result in division by zero. (I have zero recollection of why the Heawood conjecture breaks down for the Klein bottle, and it may not have been covered in that class.) So the case on the plane as opposed to, say, the torus, it was an open question.
But this is something dimly recollected from (ye gods) twenty years ago now, so I defer instantly to any of the working mathematicians or mathematicianoids.
39: "Euler" should be "Euler characteristic".
Right, so you know there's no way anyone can point to one corner of your map and say: "Aha! You can't 4-color your map because there's a problem right here." But that doesn't mean there can't be a big complicated spread-out problem. You start coloring somewhere and everything seems fine, but eventually way far away from where you started you run into a problem. You can fix that problem, but then that causes a problem somewhere else, etc. Like trying to cover the proverbial floor with a carpet that just doesn't quite work out.
38: It would be really cool if we come back in a couple days and, after a few increasingly frantic and aggravated comments, you come up with an intuitive proof. I've had a few sleepless nights where I hammered at it.
40: Ha, I'm definitely going to identify as a mathematicianoid. I'm like a mathematician, but I don't associate.
In one version of his "Theory and Practice*" talk, Knuth contrasted the relatively small amount of review and checking a long mathematical paper/proof gets compared to the process "verification" that TeX went through.
*This one touches on the concept tangentially (and why he was drawn more to computing in the end). Annoyed that I lost my copy. Somehow I thought it was from a talk he gave in Greece.
In reference to 5 and 11, I think that the author blithely saying that readers basically have to spend three months working on a project like this is actually asking a lot. You won't get any glory or publications out of being one of the ones to verify a proof like this.
Luckily, M. is actually a serious mathematician with a good track record, so people are willing to work through his claimed proof, even if they aren't going very fast. His work is actually likely to be right, unlike one other living mathematician who has claimed a proof of the Generalized Riemann Hypothesis. His case is more complicated, as he did prove an important conjecture back in the 80s, but his attempt at the GRH is (a) not widely believed and (b) has damaged his reputation.