mathematical bullshit: a confession

[gusl]

Confession time: when proving stuff, I feel the need to justify things that I consider to be intuitively obvious. In the course of this, I sometimes look up theorems in a textbook that I couldn't possibly prove, and cite them. I feel slightly dishonest when I do this.

Why? Because the proof in my head didn't need the theorem in the textbook. So why should the paper expression of my thoughts use that theorem?

I am *sure* that the statement is true but I'm unable to justify this intuitive knowledge in a formal language, without the help of the theorem in the textbook. All this talk about eigenvalues feels artificial; but it's the only way I found to connect my intuitive idea with the "objective" mathematics that "everyone" must accept.

Maybe my mind is wrong in being so secure about intuitions whose foundations it has trouble fleshing out (but I doubt it). Instead, I think that my mathematical language skills are deficient, i.e. a kind of "aphasia". If you are a visual thinker, the "informal yet rigorous" language of sentential proofs is a foreign language.

I'd say that communication is one of the hardest and most important problems faced by humanity.
See Jukka Korpela on "How all human communication fails, except by accident".

Comments

[roseandsigil.livejournal.com]

What level of mathematics do you consider "objective"? Are real numbers? Integers? Positive integers? Inductive definitions? Sets?

[gustavolacerda.livejournal.com]

I'm not going there.

[gustavolacerda.livejournal.com]

A piece of mathematics is "objective" iff a reasonable person with mathematical education must be compelled to believe it.

[roseandsigil.livejournal.com]

Gaaah!

[gustavolacerda.livejournal.com]

I am describing the reality of how humans communicate about math, and the norms they follow.

[gustavolacerda.livejournal.com]

<< the proof in my head didn't need the theorem in the textbook. >>

I should be skeptical of this. It seems likely that I am using a version of the theorem that I looked up, and I just can't recognize it as such.

[jcreed.livejournal.com]

I don't believe it's dishonest to use theorems whose proof you don't fully understand. Math is a big enterprise; delegating parts of the work to other (trustworthy) provers is fine. Anyhow while the knowledge that A implies B isn't as good as A together with A implies B, still knowing A implies B is better than nothing. (Here A = "some dead dude didn't screw up the proof of this hairy theorem" and B = "my desired corollary actually holds") The modularity of modus ponens means you can always put off really understanding the proof of A until later.

That being said, I don't find "intuitively obvious" to count for much of anything. I'm tempted to say that the entire point of mathematics is to replace one person's unanalyzable intuitive certainty that a conclusion follows from some assumptions with an argument that it does that can be examined and analyzed by anyone.

[gustavolacerda.livejournal.com]

<< I don't believe it's dishonest to use theorems whose proof you don't fully understand. Math is a big enterprise; delegating parts of the work to other (trustworthy) provers is fine. >>

I completely agree, of course.

But do you ever find yourself unsatisfied because your "informal yet rigorous"^* proof is a poor expression of your intuition, of your original reasons for believing the theorem?

^{* - by this I mean the standard of formality required by math journals, etc.}

[gustavolacerda.livejournal.com]

To borrow philosophy jargon, one could say that I'd like to unify the context of discovery and the context of justification.

[jcreed.livejournal.com]

I guess I'm a bit of a pessimist on this issue, or rather I think that it's useful to have many tools for discovery and (in a certain sense) few tools for justification. "Having few tools for justification" is a terrible way of marketing it :) but I hope you know what I mean: the fewer axioms and more highly constrained rules I used to achieve a theorem, the stronger the theorem is.

[jcreed.livejournal.com]

Ah! That clarifies what you meant my "informal yet rigorous", thanks.

But to answer your question, if my original hunch as to why a theorem is true differs from the structure of the proof, I'd say my hunch was wrong - unless perhaps there's a different, still undiscovered proof that matches it more closely.

Why should I find my unrigorous, unjustified belief that something is true more weighty than a proof?

[gustavolacerda.livejournal.com]

Not more weighty...

But by throwing out the informal bits, you may be sacrificing your readers' understanding.

Also, I'd like readers to see how I came to this hypothesis. In cases where I came to know the theorem was true before I could prove it, the "intuitive proof" precedes the hypothesis. The formalization comes after that.

[neelk]

That can't quite be right.

Take the case of the real number line. Weyl, Brouwer and a number of other great analysts have believed that the formalization of the real number line in terms of Dedekind cuts/Cauchy sequences is wrong. Note that they didn't think that the definitions and the theorems of analysis proved from it were false or erroneous -- they thought the definitions were a formalization of some concept other than the continuum, because claiming that modelling a continuum is a collection of discrete points leaves out something essential to its character as a continuum.

Since this is a perfectly intelligible and reasonable position, there has to be some extra side-condition on your claim....

[roseandsigil.livejournal.com]

To say something similar to what jcreed said below, intuition is not a reason to believe something is true. Intuition is a useful pointer to a proof that something is (mathematically) true.

(Of course, what "mathematically true" means is a different subject.)

[gustavolacerda.livejournal.com]

<< intuition is not a reason to believe something is true >>

I don't think you mean this.

[ikeepaleopard]

Is this any different than comparing pseudocode or a vague implementation strategy to actual code, where you have to deal with library details you didn't care about in order to make the code go through?

[gustavolacerda.livejournal.com]

I like the analogy. It might be correct.

[ikeepaleopard]

Proofs are programs.

[gustavolacerda.livejournal.com]

What about proofs that use excluded middle? What about proofs you'd find in journals other than JFM?

[jcreed.livejournal.com]

I think I'm with akiva in believing that it's a foregone conclusion that the analogy is correct, almost an identity.

Hoping that informal sketches of proofs should be persuasive somehow is like hoping psuedocode can be run without turning it into real code.

[bhudson.livejournal.com]

I don't feel dishonest about putting together a proof that looks almost nothing like the intuitions that led me to believe the result, but I feel sad that I wasn't able to explain an intuition that might be fruitful at helping others to come up with other useful provable results (even if they also would end up using entirely different techniques to prove it).

Case in point: I came to the idea that a particular class of quadtrees and a particular class of triangulations should intersect nicely via an understanding that they're both solving the same problem. I proved it via a weird and persnickety pair of proofs.

[gwillen.livejournal.com]

I would be interested in a handful of concrete examples of this, if you can think of them and encode them conveniently here. :-) Specifically of things which you believed to be true, but for which you resorted to some borrowed proof which didn't match your intuition about _why_ they were true.

Preferably things which are simple / accessible enough that I might conceivably have some intuition about their truth or falsity. :-)

[gustavolacerda.livejournal.com]

See Theorem 5 of my UAI paper. You may or may not find this as intuitive as I did.

[gustavolacerda.livejournal.com]

Actually, I should say that I find this proof *bureaucratic* rather than *unintuitive*. It would be more direct to avoid talk of eigenvalues... seems like an unnecessary abstraction... but our library doesn't contain theorems about cycle-products (because it's not as standard a concept), so we use the correspondence between cycle-products and eigenvalues.

[rdore.livejournal.com]

What's wrong with abstraction? It seems like saying you don't want to use a fact about mammals to prove something about your dog, you want a fact that is specifically about your dog.