Math even mathematicians don't understand (the sequel)

http://www.boston.com/bostonglobe/ideas/brainiac/2012/12/math_even_mathe.html

by ColinWright • 14 years ago

95 86 14 years ago

balsam3• 14 years ago

you know what this means? arxiv.org needs a cryogenics section, for potential resuscitation of mathematical campaigns using future technology. it'll be challenging to keep out the crackpots, though --

sillysaurus4• 14 years ago

for potential resuscitation of mathematical campaigns using future technology

What does this mean?

TeMPOraL• 14 years ago

To freeze the brains of our best and brightests in hope that future tech could let them live much longer, and possibly make some more discoveries.

taligent3• 14 years ago

It means put all of these potential solutions in a folder so that future generations (who may have been technology) can easily find them.

gtani• 14 years ago

    cryogenics section, for potential resuscitation of 
    mathematical campaigns using future technology

automated provers like coq and isabelle, I think (I also think I'm not a crackpot but ...

http://arxiv.org/abs/1211.7012

http://mathlesstraveled.com/2012/11/11/a-computer-checked-pr...

Probably the haskell/agda camp'll want to defend their honor also

merraksh• 14 years ago

Related read: Apostolos Doxiadis' novel "Uncle Petros and Goldbach's conjecture", an entertaining account of a mathematician's effort to prove the result.

edanm• 14 years ago

Very heavily seconded. One of my favorite novels, it does a really good job of giving a "feeling" of mathematics, without including any actual mathematics.

This is the same author as Logicomix, which is aslo very highly recommended - a comic about logic, Godel, and the foundations of mathematics.

http://en.wikipedia.org/wiki/Logicomix

http://www.amazon.com/Logicomix-An-Epic-Search-Truth/dp/1596... (this might be with a refferal link, I'm not sure - you have been warned :)

kenjackson• 14 years ago

No one will ever bother to read this work. There are millions of claimed proofs of various conjectures. If you want to prove Goldbach or P=NP (etc...) you either need a very simple to verify proof (not a 1,000 page proof) or you need to prove a set of interesting conjectures along the way to give yourself credibility.

In the pages of this mathematician's proof, there must be a few smaller proofs he could publish that show genuine insight, which would give him credibility. Otherwise it's just another sci.math sideshow.

balsam3• 14 years ago

true that. Say, if you wanted to modify a page on Wikiproof titled "Goldback conjecture" you have to first summarize your approach, with a tree diagram of subtheorems, and at least provide a few proofs of those subtheorems that are original, and of course, citations for those that aren't. Wikipedia for original work! It'll be fun to maintain, considering that it'll be like allowing advertisements on Wikipedia.

tinco• 14 years ago

I wonder if it's possible for an machine learning algorithm to simplify these proofs.

I take it because of the rather strict domain specificness of math papers it should be possible to develop an algorithm that can parse these papers into lemmas. Proofs normally structured as a tree of lemmas right? Or are there proofs that have more complex structure?

A single basic thing could be to extract the leaf lemmas and assert their validity. If they are valid, and the relations between the lemmas are valid then the eventual conclusion should also be valid.

Has anything like this ever been attempted? A math paper proof verifying machine learning algorithm?

jlouis• 14 years ago

Automated Therom Proving is ridiculously hard and a guess would be that it is almost impossible to train an ML algorithm to do this efficiently.

However, verifying that a proof is correct is somewhat simple, if you give the machine enough information to actually run the formalization details. In modern mathematics, this may be a necessary thing to do since nobody has time to verify these 1000 page developments anymore.

The problem is that the level of detail currently needed is very high. And this slows down the formalization process. But the area is in wild development these years, so hopefully something good comes out of it.

nairboon• 14 years ago

There are numerous projects for proof checking: https://en.wikipedia.org/wiki/Automated_proof_checking

Such an algorithm could consist of the following parts:

* a parser

* a syntax checker: to test how correct the used mathematical notation is

* if possible translate non-standard notation to standard

* using some sort of supervised learning for checking existing proofs with existing proof solvers

* manual intervention: improve translator or underlying proof solver

pdeuchler• 14 years ago

  No one will ever bother to read this work.

Yeah... but what if? Aren't you the least bit curious?

chris_wot3• 14 years ago

If it is 1000s of pages of work that is unintelligible to even killed mathematicians, then it might take years o someone's life to decode it into simpler terms.

In the end, they may find a fatal flaw, or a series of flaws and where would they be? They'd have spent a lot of time and effort to disprove a theorem that nobody was interested in.

That said, I look at the fact that there are still people working on Ramanujan's conjectures that there may still be some worth to it...

S4M• 14 years ago

I actually would like to give it a shot, even though I know that it's way too far beyond my level. But after googling Henry Andrew Pogorzelski, no pdf's came out.

I think he should have written a paper explaining in easier term what he does. E.g "First I will map the integers into a group defined by X and Y, it makes the work easier because that group has some interesting properties like... Then I show how the Goldback conjecture translates onto my group, then, etc."

I know this is easier to be said than to be done, but on the other hand the Goldback conjecture is so simple that there have to be ways to break down its demonstration (or attempts of) into understandable steps, each steps being once again broken down, etc. and each stage introducing new layers of complexity. That way, instead of claiming "I proved the Goldback conjecture, here is the proof, just check those 1000 pages", he could have said "I proved X, Y and Z, and we can see how together they can be added up to prove the actual conjecture", with X, Y and Z (and probably lots of others) being smaller results that experts could challenge or assert.

EDIT: TL;DR: If a mathematician claims to prove a long time unproven claim such as Goldbach conjecture, it belongs to him to do the vulgarisation works so even schmucks like me can have a remove idea of how he did it.

mrdmnd• 14 years ago

"Mathematicians who make big claims are obligated both to be right and to make themselves understood."

I spent most of this academic semester struggling with the material in MIT's 18.404 (Theory of Computation) class taught by Michael Sipser - at the end of one of his lectures, he mentioned that he keeps a large file of proofs on hand from people claiming to have resolved the P vs NP conjecture, but has little time or faith to read them... he calls this the "crank" file. It seems to me (and I'm just a lowly undergraduate math student, feel free to discount/discredit this) that solutions to many of the large, imposing academic challenges of our era might be found in the depths of other such professor's "crank" files.

Then again, there is definitely something to be said for establishing credentials - there's only so much time in the schedule of someone capable of verifying claims to be spent on verification, and it seems obvious that they should spend that time on solutions that come from people who have a track record of competence.

crntaylor• 14 years ago

Scott Aaronson summarizes it well when he says, of papers that have signs of being by 'cranks' --

> If I read all such papers, I wouldn't have time for anything else. [1]

Crank papers often take a long time to read, by virtue of some combination of (i) using non-standard notation and terminology, (ii) lack of familiarity with the established literature, (iii) tortured writing style.

If you claim to have proved a big new result, and you don't already have the credentials that will ensure you get taken seriously, then it is up to you to write in such a way that makes it easy for other academics to verify your work. Part of being an academic is interacting with other academics.

[1] http://www.scottaaronson.com/blog/?p=304

jseliger• 14 years ago

If you claim to have proved a big new result, and you don't already have the credentials that will ensure you get taken seriously, then it is up to you to write in such a way that makes it easy for other academics to verify your work. Part of being an academic is interacting with other academics.

This reminds me of the introduction to Thomas Kuhn's The Road Since Structure:

"Kuhn develops further the theme, which again goes back to Structure, that science is fundamentally a social undertaking. This shows up especially in times of trouble, with the potential for more or less radical change. It is only because individuals working in a common research tradition are able to arrive at differing judgments concerning the degree of seriousness of the various difficulties they collectively face that some of them will be moved individually to explore alternative (often—as Kuhn likes to emphasize—seemingly nonsensical) possibilities, while others will attempt doggedly to resolve the problem within the current framework" {Conant and Haugeland "Road"@3}.

raverbashing8• 14 years ago

Well, scan it and put it on the internet!

The usenet groups will have fun with it.

Q6T46nT668w6i3m3• 14 years ago

While correctness is preeminent, it isn't the only factor for the adoption of a proof. Coherence and intelligibility are essential. Typically, context is important too (i.e. a proof leverages a reasonable and translatable program).

While I hate that Michael Sipser uses the phrase "crank file," he's expressing an important distinction between mathematicians, computer scientists, or philosophers and, for example physical scientists: humanistic attributes are important.

P.S. You're an "undergraduate math student," not a "lowly undergraduate math student." Hang in there. :)

michaelhoffman• 14 years ago

Publications in the physical sciences need to be intelligible as well, and an elegant model is considered a plus.

losvedir• 14 years ago

solutions to many of the large, imposing academic challenges of our era might be found in the depths of other such professor's "crank" files.

Interesting, because I feel as time goes on the reverse trend will hold true. It seems to me more and more of the "easy" proofs will be discovered, leaving only those that require more sophisticated mathematical machinery. And to obtain that you will have to, at the very least, have a PhD which will leave some track record of your ability. And the better credentialed you are the less likely you'll end up in a crank file.

I took 18.404 and really enjoyed it. I remember one lecture that Professor Sipser talked about the many years he wasted battling against P vs NP. He seemed pretty cynical about it getting solved without a lot of new groundwork being laid first, and this might contribute to why he so easily tosses proposed proofs into that crank file.

ColinWright7• 14 years ago

As new proofs are distilled, understood, enhanced, and internalised, so conjectures that were previously thought out-of-reach become more reasonable. "Easy" is a relative term - many things now presented at undergraduate level were once post-doctoral work. The "more sophisticated mathematical machinery" becomes an everyday tool for the working mathematician.

tprice76• 14 years ago

The validity of a mathematical proof depends on a few very precise rules that can be checked by a computer, so I think it's interesting that we still rely so much on humans for the verification of mathematical proofs. As the article points out it's clearly problematic.

sillysaurus4• 14 years ago

Sure, but then you quickly run into the issue of, "That depends what you mean by 'rule'."

tprice76• 14 years ago

Please elaborate. I find it difficult to believe that the problem you are hinting at would be a showstopper because there already exist computer systems for verifying mathematical proofs to standards of rigor acceptable by mainstream mathematicians.

taligent3• 14 years ago

Computers aren't some magical machines that instantly understand what we mean.

At some point somebody has to write the code to implement those 'rules'. Which then opens up exactly the same problems (if not more) than if you just verified by hand.

tprice76• 14 years ago

Well, yes, we would have to convince ourselves of the validity of the code that checks the proofs. But the thing is once we made one proof checker whose code we were really confident about, the checking would be over because we could use it for any proof. Whereas with human verification of proofs each new proof is a new checking job.

foobarqux2• 14 years ago

Machine checked proofs are intractably long and are not fully automatic except for very simple problems.

tprice76• 14 years ago

What do you mean by not fully automatic? What is the manual part?

I think right now the job of describing a (sophisticated) proof to a computer is analogous to the job of writing a sophisticated computer program like a game or Facebook in assembly code. What mathematics needs is a concise language that can easily be understood by people and computers alike, like Python.

revelation• 14 years ago

See http://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_t...

tprice76• 14 years ago

Ok, what about it?

fatbird2• 14 years ago

The basic problem with your idea is that significant new proofs usually involve the invention of new branches of mathematics. It's not simply the derivation of new axioms from existing foundations (which fails for reasons outlined below because of Godel's Incompleteness Theorem), it's the laying of new foundations. For a proof checker to check it, it would need to encode those foundations, which is equivalent to discovering the proof itself.

Otherwise, given what you say, we could just let proof checkers run on clusters and stop by on Mondays to see what new discoveries have been made :)

cynicalkane• 14 years ago

I have to say something here, because this is complete nonsense.

Nothing in Godel's incompleteness theorems says that new theorems can't be found. It says theorems can't be enumerated, which actually means the opposite--there's always something new to find in a sufficiently strong system of mathematics. Not that there are theorem-enumerators of significant power in the first place.

Furthermore, proofs generally do not introduce new axioms and a proof that does, that isn't intended to be foundational, would be considered unsound.

taligent3• 14 years ago

If the Wikipedia page is correct then British publisher Tony Faber offered $1 million dollars if a proof was submitted before April 2002.

And according to this article it was submitted in March 2002.

So how come this guy didn't come forward to collect the prize ?

IvyMike• 14 years ago

The timing explains a lot.

He almost certainly came forward to collect the prize in March 2002. Along with the probably hundreds of others who also submitted 'proofs'.

revskill4• 14 years ago

Why not having a MathHub (like Github) for math, i believe even the toughest problem will have the pull request, and many people could understand the proof.

Q6T46nT668w6i3m3• 14 years ago

While it isn't version control, wiki usage has become prevalent amongst collaborators, departments, and fields.

revskill4• 14 years ago

I don't think wiki is a suitable tool for collaboration. We need small pull requests to small issue, then merging, disscussing on them, we can work parallel on multiple branches, and that means the workflow works for most of type of people.

ufo• 14 years ago

Math doesn work like that. You can't just create a git repo for PvsNP and expect that solving the problem is just a matter of accumulating enough commits. Not only does everyone involved have to know how everything works in order to come up with insight (making it hard to "delegate" subproblems) but you don't even know what subproblems need to be solved to come up with a solution!

revskill4• 14 years ago

Why not seeing "Theorems" like "Open source projects" ? I think they have the same meaning. Math theorems are the framework for other to use or extend. And they should be "open sourced", i think we don't solve the Conjecture with this "MathHub" but it will get solved and understandable by anyone who're interested in a time.

Someone• 14 years ago

https://github.com/c-corn/corn (via http://coq.inria.fr/cocorico/List%20of%20Coq%20Math%20Projec...)

This is for CoQ, which is only one of many theorem provers/checkers. Differences between them aren't only notational; they also can also be in the set of axioms they build from.

I don't believe what you believe though. Certainly, the 'many people could understand the proof' is only true in the 'could, if they were willing to spend years studying them' sense. For example, I think I could understand Wiles' proof of Fermat's last theorem, but as it stands, I bet it could take me a month to even understand what its first paragraph is talking about. There will be thousands, maybe even millions, of people in the same boat.

revskill4• 14 years ago

I don't think so. For example, great project at Github's got success based on great documentation. Mathematical theorem's proofs are also delivered with full documentation. It's called documentation when implicitly anyone interested in can understand the documentation. For the Wiles' proof, we don't know the proof/theorems in it before we know it. In short, we need standards to the modern math.

jmount• 14 years ago

This type of behavior was well documented in Underwood Dudley's "A Budget of Trisections." The problem is obsession and a deliberate cultivation of the ticks the public associates with genius are much more common than actual breakthroughs.

robryan• 14 years ago

I think this has an analog in software. The massive enterprise/ government systems which get bogged down for years and become almost impossible to replace.

Will be interesting to see if newer generations embrace collaboration and new technology more or will things still get pushed forward by the lone and difficult to understand outlier who becomes at least convincing enough for others to trawl through their complicated texts.

I guess issues of credit would have weighed into this method. In this case, if intermediate findings were published in a simple to understand way they may have attracted enough interest to be beaten to the final proof?

nnq4• 14 years ago

How hard would it be to write mathematical proofs in a modular way? And have someone check a "module" of a proof and someone else another "module" and so on?

...and for the bits that's possible, write in a subset of mathematical language that computer can check, or at least partially check and ask the human reviewer for feedback on the parts that can't be automatically proven.

I always fount it odd that mathematicians use so little of the mind augmenting potential of computers. Is is true that there aren't any smart enough programmers to craft the tools they would need, or that the tools end up being so "user hostile" that they always go back to pen and paper? I know people tried to express physics proofs in "computer-like language", Sussman et all in Structure and Interpretation of Classical Mechanics, but I've never heard of such things really catching on and being actively used and developed by mathematicians.

12characters• 14 years ago

> How hard would it be to write mathematical proofs in a modular way? And have someone check a "module" of a proof and someone else another "module" and so on?

To a large extent, this is what we do. But of course, modules by themselves don't prove a thing about what we're originally interested in so that not one module can stand by itself as any advance in the proof, that theconclusion of any module of the proof are surely needed for all the others modules to make sense and that these conclusions are more often than not formulated in a new part of language (new words, concepts, and rules to play with them) introduced in said module. Parallel work of the sort I infer you have in mind might be possible in some instances, but there is so very few of them in my opinion that it's just not worth trying.

> ...and for the bits that's possible, write in a subset of mathematical language that computer can check, or at least partially check and ask the human reviewer for feedback on the parts that can't be automatically proven.

No can't do: in mathematical writing, what is actually written is the tip of a gigantic iceberg of implied reasoning and background scenery. There might be a way to make computer understand this, but as far as I know it has yet to be found. That, and making explicit what is not in mathematical writing would make the length of any proof grow manymanyfold - and I actually mean manymany....manyfold.

nnq4• 14 years ago

> in mathematical writing, what is actually written is the tip of a gigantic iceberg of implied reasoning and background scenery

The programming equivalent of this as I see it is a program depending on lots of libraries encapsulating that "implied reasoning". And you can manage a program even with tens of millions of lines of code in libraries. And it doesn't make the program itself larger because that library code is reusable, you can also use it in other proofs. Yes, it's incredibly hard to manage such a code base, you also need extensive documentation, something like "literate programming" - but it's not intractable.

You would have to write a big part of mathematics as library code, probably a multi-decade length project - but the benefits seem huge! "Translating" mathematics in such a form could augment a mathematicians brainpower "manymany....manyfold" and could be just as important as, let's say, a cancer research project taking decades and tens of millions in funding, but it should worth it! Imagine that hundreds of "less talented" mathematicians could handle problems that only a handful of people can understand today (with the guidance of the "real geniuses", of course), revolutionizing many fields of science through the consequences of their results.

As an analogy, when people used roman numerals, only a handful of highly educated people could do complex calculations, but nowadays we all have more than basic arithmetic knowledge, thanks in large part to a "change of language". I think a "change of language" could really make mathematics a less "elite only" field (though I have greater hopes for letting "AI systems" give a helping hand than for letting "lesser mathematicians" do some of the work, in the end one can't predict what will make the most difference - hardware or wetware, it's still computing power, and, as the complicated software problems are solved, more and more of the computing power can translate into "mathematical reasoning power" I think).

hexagonc• 14 years ago

You mean like Mathematica? Or Wolfram's "predictive interface", http://reference.wolfram.com/mathematica/guide/WolframPredic...?

CurtMonash3• 14 years ago

So many of these proofs are of the form:

1. Assume the desired conclusion is false. 2. Make an error. 3. Derive a contradiction.

And by the way, most mathematicians have made plenty of bad proofs. I told my thesis adviser I had a "proof" months before I actually did. Years before that, I found a short proof of Fermat's Last Theorem (which was however too long for the margin of my book ...).

Generally, the way "big" proofs go is that there's a whole lot of new mathematics, and some handwaving at various points along the way. Then the work starts of checking whether the handwaves are actually accurate. The better the mathematician, the more likely it is that they actually are ...

raverbashing8• 14 years ago

Yes

Because proofs (or disproofs) by contradiction are "the easy way out"

Proving something is right is much harder if not impossible (hi Mr. Goedel)

CurtMonash3• 14 years ago

That wasn't my point. Rather, I was suggesting that proofs by contradiction can easily be in error (because if you make an error, you have a good chance of eventually getting to your contradiction).

Anyhow, when I did mathematics, I didn't run into people caring about proof by contradiction vs. direct proof. However, I did occasionally run into a preference for constructive vs. non-constructive proofs. E.g., my thesis used a prior result that included a funky existence proof, and my adviser pushed me to find an alternate proof that was directly constructive.

teeja• 14 years ago

For a similar fate in the physics world, WP: Arthur_Eddington#Fundamental_theory. Which demonstrated that it's not enough to have an idea, you have to find some kindred souls with the stamina to be your soundboard - everyone else will be looking for any excuse to avoid the confrontation.

E.g. dare to suggest that the universe <i>might not</i> be simple, after all.

Math even mathematicians don't understand (the sequel)

Related Stories