Mathematics desk
< August 25	<< Jul \| August \| Sep >>	August 27 >

Welcome to the Wikipedia Mathematics Reference Desk Archives
The page you are currently viewing is an archive page. While you can leave answers for any questions shown below, please ask new questions on one of the current reference desk pages.

August 26

Computer-aided proofs since Appel-Haken

This is less about mathematics than about mathematics history. I'm interested in knowing what notable questions in mathematics there have been whose solution have relied upon an effectively not-by-hand-checkable computer program since Appel and Haken proved the Four-Color Theorem using a computer program in 1976. —Preceding unsigned comment added by Julzes (talk • contribs) 08:22, 26 August 2009 (UTC)[reply]

What do you accept as "proved"? The Kepler conjecture has most likely been proved by computer, but nobody is completely sure if that proof is sound. There are several proofs now that have been found by automated reasoning systems - the most famous one is probably the Robbins conjecture proved by EQP. However, that proof was hard to find, but easily checkable. --Stephan Schulz (talk) 09:03, 26 August 2009 (UTC)[reply]

I'm mostly interested in the question of exhaustive searches and other sorts of things where the acceptance of effectively uncheckable computer calculations is involved. The Kepler Conjecture is a good example, but the fact that it's controversial sort of goes against what I would have proposed saying about the acceptance of things similar to the proof of the Four-Color Theorem having become somewhat routine.Julzes (talk) 10:08, 26 August 2009 (UTC)[reply]

Well, sorry if reality does not support your proposed opinions ;-). If you are interested in searches: The claim that the game-theoretic value of Checkers is 0 comes from exhaustive calculations by the Chinook team, and seems to be widely accepted. --Stephan Schulz (talk) 10:33, 26 August 2009 (UTC)[reply]

A lot of work has been done on formalizing proofs that have already been found by humans (the Flyspeck project is an example, as is Gonthier's Coq implementation of the 4-color theorem). There is also lots of exploratory math done with computers--see some of Doron Zeilberger's articles on experimental math for info. But I think not all that much has been done using computers to find proofs of traditional math conjectures. WZ theory might be an example though--a scheme for automatically solving certain hypergeometric sums. Hmm, another example, the Bailey-Borwein-Plouffe formula for computing digits of pi was found with a big computer search involving the PSLQ algorithm (there are related such formulas too, found in similar ways). This page is a reasonable place to look for info about formalized math in general, and there was a special issue of AMS Notices about formalized math, that has several good articles that you might like.[1] —Preceding unsigned comment added by 67.122.211.205 (talk) 23:39, 26 August 2009 (UTC)[reply]

I should add that the point of Gonthier's proof of 4CT is that (unlike Appel-Haken's) it can be checked by a program that itself is supposed to be hand checkable (Coq's proof checking core is based on a small, hand checkable kernel, per the de Bruijn criterion). 67.122.211.205 (talk) 00:01, 27 August 2009 (UTC)[reply]

Further: OK, I think I understand your question better now. The issue with the Appel-Haken proof is it was done with 1970's computer and software technology, and was a huge complicated set of C assembly language programs that were potentially full of bugs and was too large to be inspected by hand (being small enough for hand verification is called the de Bruijn criterion), so nobody could be sure it was really right. These days, programming itself (at least at this pointy-headed level) is getting more formalized, so in a language like C you can write a program with the intention that it computes X, and make informal arguments that it actually does compute X, but maybe your arguments have a gap and your program has bugs. But in a language like Coq (you can view Coq as a programming language), the programs are stated rigorously enough that you can prove theorems about their properties, and mechanically verify the proofs, using a hand checkable verifier. So you can write a Coq program that computes X, and state what X is, and prove as a theorem (formally verified) that your program really computes X. That is essentially Gonthier's proof of 4CT, I think. (There is an article about it in the AMS issue I linked to). In principle you could repeat Schaffer's calculation of the outcome of checkers, by writing a Coq program that computes the outcome of checkers, proving its correctness, and running it for however long it took (hmm, I guess that involves trusting the compiler, but we are getting closer to having completely verified compilers), and then saying the output is verified. In that way we're getting away from the acceptance gap that the Appel-Haken proof faced. Anything we can compute unverifiably, we can do verifiably with enough extra work. 67.122.211.205 (talk) 00:12, 27 August 2009 (UTC)[reply]

Thanks for the thoughtful answers. Aside from helping me help someone else write a short piece on the 4CT, it's a subject of some personal interest, so I will be having a look at what you have offered up.Julzes (talk) 03:56, 27 August 2009 (UTC)[reply]

Connect Four has been shown to be a first player win using a computer-assisted search approach. Victor Allis's Master's Thesis contains a very interesting and clearly written account of the investigation. Some people may have the impression that a computer-assisted proof involves writing an enormously complex and poorly understood program which then runs for hundreds of hours before producing a one-line answer. This is not the case. The programs in such proofs are re-written and expanded many times, as the researchers' ideas evolve. Each new version of the proof program can be checked by ensuring it reproduces the partial results of previous versions - indeed, this is a very efficient form of regression testing. In addition, the proof program (or suite of programs - the tasks of generating and evaluating cases may be divided between different programs) can be expected to include a degree of redundancy and internal cross-checking - the equivalent of check sums. It should also store snapshots of intermediate positions or results, which can be checked for internal consistency by independent programs. The algorithms behind the proof programs should be described so that they can, in principle, be implemented independently in entirely different software. And finally, improvements to the original algorithms are often made and tested by later researchers, which provides the ultimate error check. The original Appel-Haken proof of 4CT, for example, has evolved through several subsequent generations, each improving on the efficiency of the previous generation, but all confirming the original result. Gandalf61 (talk) 12:01, 27 August 2009 (UTC)[reply]

Definition of Kähler manifolds

From the Wikipedia article about Kähler manifolds, a Kähler manifold is a complex manifold with a Hermitian metric $h=g+i\omega$ where $g$ is a Riemannian metric, $i$ an almost complex structure and $\omega$ a symplectic form, which must satisfy an additional condition.

The article gives two of such equivalent additional conditions:

$d\omega =0$ , the symplectic form is closed.
Parallel transport induced by the Levi-Civita connection corresponding to $g$ actually induces $\mathbb {C}$ -linear mappings of tangent spaces, not only $\mathbb {R}$ -linear.

I've been thinking about this for a while now but I can't seem to figure out the equivalence. For example, starting with the second condition, I have no idea how to involve $\omega$ .

I'd be very grateful if anyone had a few tips or a good reference. Thanks. -Xedi^Talk 13:52, 26 August 2009 (UTC)[reply]

can u solve this

1=19-20=60

one straight line --America vega (talk) 21:23, 26 August 2009 (UTC)[reply]

What is the question? You have given a false arithmetic statement and a geometric object, you haven't actually given us anything to solve. --Tango (talk) 21:29, 26 August 2009 (UTC)[reply]

I know my brother gave it to me to solve but I can't I think it might be a riddle--America vega (talk) 21:39, 26 August 2009 (UTC)[reply]

is it (1,20) (20,60) which is y=40x/19+17+17/19 ? 83.100.250.79 (talk) 21:45, 26 August 2009 (UTC)[reply]

How many matchsticks can you move? – b_jonas 11:53, 29 August 2009 (UTC)[reply]

Commutivity of addition

Resolved

– Wow! Good work everybody.

Has anyone any idea how one might prove the commutivity of addition?

Let's start with a + b = b + a where a and b are real numbers. ~~ Dr Dec (Talk) ~~ 23:14, 26 August 2009 (UTC)[reply]

This will depend on your preferred Construction of the real numbers. Algebraist 23:15, 26 August 2009 (UTC)[reply]

Good point! Okay, let's list the possible constructions and their respective proofs... ~~ Dr Dec (Talk) ~~ 23:21, 26 August 2009 (UTC)[reply]

The reals are a Field (mathematics). The additive operation of a field is commutative by definition. QED. ;-) --Stephan Schulz (talk) 23:24, 26 August 2009 (UTC)[reply]

This is a joke, right?! PROVE that addition is commutative! ~~ Dr Dec (Talk) ~~ 23:27, 26 August 2009 (UTC)[reply]

Only slightly. The most common definition of the reals is as the essentially unique ordered field satisfying a completeness property (exactly how the completeness property is phrased varies); with this definition, commutativity of + is automatic. Algebraist 23:30, 26 August 2009 (UTC):[reply]

There are a great many constructions of the reals, and I doubt we could find them all, let alone list them. For many constructions, the commutativity of addition is a trivial consequence of the commutativity of rational or integer addition; this is the case for every construction listed in our article, for example. Algebraist 23:30, 26 August 2009 (UTC)[reply]

Okay, my first example was that of the reals. What about the addition of connexions? What about group rings? (Can you PROVE the commutivity instead of ASSUME it? Can you PROVE it from the properties that are not derived from the assumption itself?) ~~ Dr Dec (Talk) ~~ 23:40, 26 August 2009 (UTC)[reply]

I think "prove addition is commutative" makes the most sense when you're discussing addition of the natural numbers. More complicated structures like the reals are constructed and artificial and commutativity of addition is usually taken as an axiom (Archimedean complete ordered field) rather than something to be proved (unless you're discussing a specific construction of reals, such as Dedekind cuts). The basic properties of the natural numbers are usually given as the Peano axioms. They say that every natural number N has a successor S(N), and they define addition by saying A+0=A and A+S(B)=S(A+B), plus a few other things. From these axioms, the commtativity of addition should be provable as a theorem. 67.122.211.205 (talk) 23:49, 26 August 2009 (UTC)[reply]

67.122.211.205, you're half way there. Now prove it... ~~ Dr Dec (Talk) ~~ 23:55, 26 August 2009 (UTC)[reply]

It needs an inductive proof. Addition is "only" an inductive theorem of the natural numbers. Via induction, the proof is fairly simple. --Stephan Schulz (talk) 23:59, 26 August 2009 (UTC)[reply]

Even with the naturals, there are alternative approaches. For example, if we instead define the naturals to be the finite cardinals, then commutativity of addition is a triviality. If we define the naturals to be the nonnegative (or positive, to taste) part of the essentially unique well-ordered integral domain, then commutativity of addition is again true by definition. Algebraist 00:05, 27 August 2009 (UTC)[reply]

But that's my hang-up: you're ASSUMING it as a definition. Something doesn't sit very well with me about this axiomatic aproach to mathematics. Lots and lots of assuming makes many many things matters of definition. For example, as the axiom article says: "...non-logical axioms (e.g., a + b = b + a) are actually defining properties for the domain of a specific mathematical theory (such as arithmetic)." So the natural numbers are defined, arithmetic is defined. They are not provable; simply defined and accepted. ~~ Dr Dec (Talk) ~~ 00:22, 27 August 2009 (UTC)[reply]

Yes, so? This is the usual way of defining mathematical systems since Hilbert; you define a system by its key properties, and call those properties axioms for the system. It is of course possible to go the other way, and define your system to be some specific object in some other system (usually a set theory of some sort) and prove that the object you've chosen has the key properties you want, but this is rather artifical. After all, if the object you'd decided was the real numbers turned out not to have commutative addition, then that wouldn't say anything interesting about the real numbers. It would just mean you'd picked the wrong object to be them. Algebraist 00:33, 27 August 2009 (UTC)[reply]

It may be artificial, yes, but on the flip side, actually constructing the object of interest (set of real numbers, set of natural numbers) in terms of other, well-accepted theory, provides one clear way of proving the existence of that object. Declan does have a point that simply making a list of properties of real numbers is not very satisfying until you can prove that a set of numbers, together with appropriately defined addition and multiplication, actually exists.

Of course, this has been done time and time again with the real numbers, most notably with Dedekind cuts and Cauchy sequences. --COVIZAPIBETEFOKY (talk) 00:45, 27 August 2009 (UTC)[reply]

Another point that should perhaps be made is that those constructions do depend on some framework of set theory, so if you don't accept set theory, then these hardly suffice as constructions. The fact is, however, that you have to start somewhere, and in the predominant view, ZFC is accepted as the basis for nearly all of mathematics. --COVIZAPIBETEFOKY (talk) 00:50, 27 August 2009 (UTC)[reply]

I didn't mean to disparage embedding things in set theory in general, but rather the relevance of the practice to the question at hand. Implementing real numbers as Cauchy sequences is a worthwhile pursuit for a number of reasons, but it doesn't do much to elucidate the commutativity of real addition, and shouldn't really be considered a proof of said commutativity. Algebraist 00:55, 27 August 2009 (UTC)[reply]

I think you're missing Declan's point here. Sure, you can take the synthetic approach to defining real numbers, and then - duh! - addition is commutative. However, the synthetic approach makes the assumption that the set of real numbers satisfying all of those properties exists in the first place. This has to be proven first, which can easily be done by way of Dedekind cuts or Cauchy sequences.

The biggest hurdle in proving commutativity of addition in the set-theoretic constructions of natural numbers, integers, rationals and reals is proving that it is so for the natural numbers, and Carl has outlined that part below. --COVIZAPIBETEFOKY (talk) 01:10, 27 August 2009 (UTC)[reply]

From a certain perspective, "constructions" of number systems in set theory do not increase our confidence in the consistency of those number systems. Set theory is important as a foundational system because many systems of interest can be formalized within it. For example, we may argue in favor of set theory because we can formalize the real numbers within it. But this argument presupposes that we already know what the real numbers are, so that we can test whether they can be formalized within set theory. — Carl (CBM · talk) 01:18, 27 August 2009 (UTC)[reply]

(edit conflict) I take the point, but I don't think there's any avoiding it. The same applies to constructive approaches: you make up a definition, carefully making sure your definition ensures all the properties you want, and – duh! – addition is commutative. A better question might be "What is it about what we use the real numbers for that makes us want to force addition to commute?". One possible answer would be that a fundamental use of real numbers is to measure physical magnitudes, such as lengths of line segments, and there's a natural geometric way of adding lengths of line segments which is commutative. I have not thought much about this and have no idea if this is a very good answer. Algebraist 01:20, 27 August 2009 (UTC)[reply]

Declan, could you clarify exactly what your hang-up is here? If it's that you're assuming that a set of "real numbers" exists that satisfies all of its supposed properties, this can be proven - under the assumption that we accept the axioms of set theory. The fact that we have to assume something is an inescapable fact of mathematics, due to Godel's theorem.

If it's closer to what Algebraist is saying, in that you want justification for the assumption of commutativity of addition, well, you have Algebraist's answer here. --COVIZAPIBETEFOKY (talk) 01:36, 27 August 2009 (UTC)[reply]

Wow! I'm amazed by the thought provoking discussion that has taken place while I've been lazily snoozing. I'm not sure how to frame my problem in the language used above. My basic problem is that no-one seems to be able to prove that m + n = n + m for all, let's make it simple, natural numbers m and n. We know that the natural numbers exist: we can count with them! So I'm not sure that the existance of the natural numbers is a problem. My problem is the assumption that the natual numbers have the property that m + n = n + m. It seems that we do have to start with some axioms. I'm not sure how to phrase this, but if we removed any mention of the commutivity of the natural numbers and any properties directly implied by commutivity then could we prove the commutivity of the natural numbers? Can we prove, without first assuming, that m + n = n + m? ~~ Dr Dec (Talk) ~~ 11:58, 27 August 2009 (UTC)[reply]

Yes. It is possible (though not exactly easy) to prove, from the axioms of peano arithmetic, that addition is commutative. Carl has already addressed this below.

If we choose to use some particular set-theoretic model of natural numbers, it may turn out to be easier to prove, depending on the model. For example, it is really easy to prove commutativity of addition if we choose to define natural numbers as finite cardinal numbers. --COVIZAPIBETEFOKY (talk) 12:23, 27 August 2009 (UTC)[reply]

And now Shahab has also addressed the same problem. --COVIZAPIBETEFOKY (talk) 12:26, 27 August 2009 (UTC)[reply]

Declan is this what you want: In what follows I assume ZFC. N (the set of natural numbers) is defined as the smallest successor set. Assume associativity in N has been established. If not that too can be easily proven.) Let

M=\{n\in N:1+n=n+1\}

. Clearly

1\in M

. Suppose that

n\in M

. Then

1+n^{+}=(1+n)^{+}=(n+1)^{+}=(n^{+})^{+}=n^{+}+1

. Thus

n^{+}\in M

and hence by the principle of induction M=N and so n+1=1+n for all n in N. Let

M'=\{n\in N:n+m=m+n\forall m\in N\}

. We have shown 1 is in M'. Assume n in M'. Then

m+n^{+}=(m+n)^{+}=(n+m)^{+}=n+m^{+}=n+(m+1)=n+(1+m)=(n+1)+m=n^{+}+m

. Thus

n^{+}\in M'

and so M'=N. Regards--Shahab (talk) 12:19, 27 August 2009 (UTC)[reply]

Expanding on what Algebraist said: In the axiomatic approach, we take an object and choose a system of axioms that describe it to a greater or lesser extent. If we can prove some property of the object from those axioms, all that this shows is that the property in question is a logical consequence of those axioms, and thus no additional information about the object is needed, apart from the axioms, for us to know it has the property in question. In a certain sense, however, such a proof does not really tell us anything "new" about the system, because we already knew (or assumed) that the object satisfies the axioms, and thus we had already implicitly assumed that the object has every property that is a consequence of the axioms. In this sense, we only learn "new" things about an object when we learn that some property possessed by the object is not a consequence of the axioms we had been studying. — Carl (CBM · talk) 01:12, 27 August 2009 (UTC)[reply]

Maybe I'm misunderstanding what you're saying, but isn't the entire endeavor of mathematics to discover new logical consequences of axioms? Just because a property follows from the axioms doesn't mean it's trivial. Conversely, how can we learn things about an object that aren't predicated on the axioms? If a claim doesn't follow from the axioms, isn't it invalid? Rckrone (talk) 06:32, 27 August 2009 (UTC)[reply]

Yes, one part of the endeavor of mathematics is to discover new logical consequences of the axioms, and these consequences can be very non-obvious and difficult to determine. However, from a different viewpoint, once we have made the leap of accepting a certain collection of axioms, we have implicitly also accepted all logical consequences of those axioms, and thus when we prove a new theorem from the axioms we do not need to ask people who already accept the axioms to accept our new theorem as well.

Now, there is a distinction between a mathematical object itself, and the axioms used to study it. Finding proofs from axioms that an object satisfies is one way to discover properties of the object that we didn't already know. But, for example, there are many properties of the natural numbers that are not provable in Peano arithmetic, or even in ZFC. This non-provability doesn't make these properties invalid, it makes them interesting. — Carl (CBM · talk) 10:22, 27 August 2009 (UTC)[reply]

A further note that I think may be linked with Declan's doubts about the axiomatic approach, above. It is probably true that axioms do not give a complete or explanatory description of what they are talking about (probably due to a close reason, reading an article is not as clear as talking with the author). But I'd say that the main use of axioms in modern maths is more about recognizing known objects, rather than describing new ones --what makes an object more familiar is using it. That is, they are useful to detect known structures into new ones; in particular, in the middle of the jungle of an unknown problem under study. Your nose sniffs something familiar; you formalize it checking that a certain set of axioms is satisfied, and you immediately have at disposal all theorems and results in a given discipline (this is, by the way, a good reason why, as a mathematician, you can't allow yourself to completely ignore areas outside your field). From this point of view the introduction of the axiomatic method is like the invention of the prêt-à-porter : no more need of clothes made to measure! (oops, unintentional). Indeed, the meaning of "axiom" is not "a self-evident proposition" as sometimes people say; it's from the Greek word ἀξίωμα, and may be explained as "what makes something worth of being given a certain name". --pma (talk) 13:38, 27 August 2009 (UTC)[reply]

To prove that addition is commutative in Peano arithmetic, one proceeds in the only way possible, which is by induction. One first proves that addition is associative and that, for all a, 1 + a = a + 1. Then one proves by induction on b that b + a = a + b. The key string of equations is:

a+(c+1)=a+(1+c)=(a+1)+c=(1+a)+c=1+(a+c)=1+(c+a)=(1+c)+a

— Carl (CBM · talk) 00:51, 27 August 2009 (UTC)[reply]

To get at what I think the point of Declan's question is, we arrive at mathematical axioms through abductive reasoning and I don't know of any escape from that. There are various systems of logic like ludics that try to be somehow more primitive than Hilbert-style deduction but AFAIK that doesn't help at the very bottom. 02:28, 27 August 2009 (UTC) —Preceding unsigned comment added by 67.122.211.205 (talk)

Thanks to everyone for their input. I've enjoyed reading your comments very much. I'll sign of this thread now because I'm satisfied. That doesn't mean that someone can't start a sub-thread. In fact I'd quite like to see one. Thanks again! ~~ Dr Dec (Talk) ~~ 12:30, 27 August 2009 (UTC)[reply]

More on the commutivity of addition

Declan Davis asks, "Can we prove, without first assuming, that m + n = n + m?". The answer to this in the naive sense is yes. For example, the axioms of Peano arithmetic do not include the desired theorem as an axiom but do imply the theorem.

But there is a deeper level of analysis at which the answer is "no". If we assume a set of axioms for arithmetic which imply commutativity of addition, then we are at the same time implicitly assuming the commutativity of addition, along with all other the logical consequences of those axioms. One could ask if commutativity of addition is provable from logic alone, with no axioms at all: it is not, because there are many structures with a single binary function symbol interpreted by a non-commutative function. Thus some additional axioms will be required to establish commutativity, and at the moment we assume those axioms to be true we are also committing ourselves to the fact that addition is commutative.

A parallel example uses the axiom of choice (AC) and ZF set theory. In ZF, we can prove many theorems of the form "If Θ then AC". But none of these theorems actually proves that the axiom of choice holds. In order to obtain AC itself as the conclusion of a proof, we must introduce some assumption (Θ) that implies AC, at which point we have implicitly already assumed AC. — Carl (CBM · talk) 14:40, 27 August 2009 (UTC)[reply]

Good point, well made. ~~ Dr Dec (Talk) ~~ 15:14, 27 August 2009 (UTC)[reply]

Also on proving from axioms not being everything, you might be interested in the opposite endevour - getting axioms from your theorems which is what Reverse mathematics tries to do! Dmcq (talk) 15:12, 27 August 2009 (UTC)[reply]

An example of a theorem of commutativity (of multiplication) in algebra is of course Wedderburn's little theorem. --pma (talk) 15:45, 27 August 2009 (UTC)[reply]

Associativity of composition

Has anyone any idea how one might prove the associativity of composition?

Let's start with real valued functions f, g and h. How do we prove that $(f\circ g)\circ h=f\circ (g\circ h)?$ ~~ Dr Dec (Talk) ~~ 23:14, 26 August 2009 (UTC)[reply]

This is true essentially by definition:

((f\circ g)\circ h)(x)=(f\circ g)(h(x))=f(g(h(x)))=f((g\circ h)(x))=(f\circ (g\circ h))(x)

. Algebraist 23:18, 26 August 2009 (UTC)[reply]

Yeah, I agree. (I was going to leave a note saying that this one was easier, but I was busy reading your post on the addition problem). Good work Algebraist.

...of course, it misses an "for all x" quantifier, and you need to assume Extensionality . --Stephan Schulz (talk) 23:28, 26 August 2009 (UTC)[reply]

It's not extensionality that is used but the definition of equality of functions. The proof does not depend on functions being implemented as sets in any particular way, or indeed at all. Algebraist 00:11, 27 August 2009 (UTC)[reply]

You do need to assume extensionality, but not in the set theoretic sense. What is ordinarily called "equality of functions" is more precisely extensional equality of functions. In systems with intensional equality, function composition generally not associative in the sense described above. In systems with extensional equality, the proof is immediate, as shown above. — Carl (CBM · talk) 00:43, 27 August 2009 (UTC)[reply]

Good point. Algebraist 00:47, 27 August 2009 (UTC)[reply]