Real mathematics is (or at least should be) algorithmic. The axiomatic method is like machine language or a Turing machine or a Tuxedo. It is very stifling.

February 18, 2009 9:32 AM

One night, very late, I was browsing the internet, using my current computer, Shalosh B. Ekhad, III. I was searching for "Ekhad". All of a sudden, to my amazement, I chanced on a website whose last update was Sept. 30, 2050, and found this little Elementary Geometry textbook. This text may seem a bit strange to 2001 humans. It appears that there are no proofs, only statements, in Maple, using English-based names for the definitions and theorems. But THE STATEMENT IS THE PROOF, ready to be run on Maple, that will output "true" if the proof-statement is correct, and "false" otherwise.

Example: Napoleon's theorem, involves two definitions: ItIsEquilateral and CET. ItIsEquilateral involves DeSq. DeSq is primitive. CET uses Circumcenter, Circumcenter involves the primitive definitions Ce, and Center. Hence in order to understand the statement of Napoleon's theorem you only need to look up the definitions: Ce, Center, CET, Circumcenter, DeSq and ItIsEquilateral, and get a completely self-contained statement of the so-called Napoleon Theorem. Then to prove it, first download RENE, then get into Maple by typing: "maple" (without the quotes); once inside Maple, type: "read RENE;" (without the quotes), and then "Napoleon();" (without the quotes). You should immediately get the response of the computer: true.

posted by orthogonality (42 comments total)

whuh?
posted by Saxon Kane at 9:35 AM on February 18

I love the smell of non-euclidean geometry in the morning.
posted by FatherDagon at 9:38 AM on February 18

They're still using Maple in 2050? Looks like there's no hope for the future.
posted by backseatpilot at 9:39 AM on February 18 [1 favorite]

During breaks while writing, the team enjoyed bracing rounds of Hybrid.
posted by jbickers at 9:40 AM on February 18

And a student copy of Maple is only $100!
posted by jedicus at 9:41 AM on February 18

This sounds terribly confusing. But if I read it correctly, the point being made is that mathematical theorems can be expressed in a form a computer can execute, and correct execution is equivalent to proving the theorem. Which is no surprise if you followed mathematical logc, but it's fun to see it actually done.

Either that or this is Time Cube nonsense; I didn't spend enough time looking at actual theorems to be sure. That's the fun about professional academic mathematics, the line between brilliant and crazy is not particularly clear.
posted by Nelson at 9:53 AM on February 18 [3 favorites]

Real mathematics is (or at least should be) algorithmic. The axiomatic method is like machine language or a Turing machine or a Tuxedo.

This word, algorithmic... I don't think it means what you think it means.
posted by Iosephus at 10:00 AM on February 18

what it all means
posted by poppo at 10:06 AM on February 18

OK, so picking an easy one to decode there's the triangle centroid theorem. That's the one that says that lines drawn from the side midpoints to the opposite angle all meet at a single point. This theorem uses 3 definitions: midpoint, line and "concurrent". The midpoint and line are pretty simple and easy. But "concurrent" is a linear equation solver. Given 3 lines, it returns true if they intersect. That's not a proof, that's a demonstration.
posted by DU at 10:07 AM on February 18 [2 favorites]

Iosephus , I think his point is that a Turing Machine is an idealized computer, using only a small set of primitive operations. While it's a pure representation of the universal computer, nobody writes serious code for a Turing machine, as it would be far too tedious.
posted by orthogonality at 10:08 AM on February 18

what
posted by zsazsa at 10:09 AM on February 18

Doron Zeilberger is a hoot. His "Opinions" are equal parts proselytizing and grumpy kvetching, with some significant overlap. He's probably the most visible experimental mathematician (second, maybe, only to V. I. Arnold). He really deserves more of a post. (Nothing wrong with this one, orthogonality, just that there's more to say.)
posted by gleuschk at 10:09 AM on February 18 [2 favorites]

the point being made is that mathematical theorems can be expressed in a form a computer can execute, and correct execution is equivalent to proving the theorem. Which is no surprise if you followed mathematical logc, but it's fun to see it actually done.

Computers can and do create mathematical proofs in ways that humans cannot, such as the method used to create a proof of the four color theorem. It was proven in 1976, but in the years that have passed since then mathematicians have done little to improve on the massive brute force proof other than trimming it down some. To some extent, a computer-generated proof is useful, because the proven theories can then be safely used as the basis for new theories, but coming up with an elegant human-understandable proof usually does a lot more to illuminate how the mathematical system in question works.
posted by burnmp3s at 10:10 AM on February 18

Storytime. There is a famous sequence, the name of which I shall deliberately omit. It goes: 1, 11, 21, 1211, 111221, 312211, and so on. Can you guess the next one? (Hint: try reading aloud.)

John Conway defined and studied the "weird and wonderful chemistry of audioactive decay" of this sequence in the 1980s. He found that the sequence eventually decomposes into combinations of only 92 string "elements", which he promptly named after chemical elements. An element in one term decays only into other elements in the subsequent term. Moreover, this decomposition into elements happens in a finite (double-digit) number of steps. This is known as Conway's Cosmological Theorem. Two independent proofs were produced, but were unfortunately lost.

But to the rescue come Shalosh B. Ekhad and his human co-author, Doron Zeilberger! In 1997 they proved the Cosmological Theorem, and everything was right in math again.
posted by parudox at 10:12 AM on February 18 [6 favorites]

Oh wait, Maple can do symbolic manipulation, IIRC, so I guess that's a proof after all. Or could be.
posted by DU at 10:12 AM on February 18 [1 favorite]

...(second, maybe, only to V. I. Arnold). He really deserves more of a post...

Whoa gleuschk!! V.I. Arnold! I hadn't heard that name since college and trying to make my way through his Mathematical Methods. I swear I just broke into a cold sweat...
posted by vacapinta at 10:19 AM on February 18

Still, if imperative programming is a gross bastardization of what they're using Maple for, the way they're using Maple is a gross bastardization of PROLOG.
posted by 7segment at 10:20 AM on February 18 [1 favorite]

This link has led me to find a wonderful link.

Rejecta Mathematica is a real open access online journal publishing only papers that have been rejected from peer-reviewed journals in the mathematical sciences.

posted by DU at 10:23 AM on February 18 [2 favorites]

orthogonality, alrighty then, he's not confused. But I join the above posters in that he's a bit confusing.

I'm not familiar with Maple's solver engine. Hence I wonder if like hinted above by DU there isn't something fishy going on here. (And let's not get into the hairy bits about this whole business depending on just assuming algebraic geometry AND that Maple's engine is a sound implementation of it, where I'm using sound in its technical sense).

Just professional (de)formation, all this nitpicking, sorry. ;-) I'm just as big a constuctivist and cheerboy for experimental mathematics as you'll find around, mind you. The skepticism, it comes with the morning coffee!
posted by Iosephus at 10:24 AM on February 18

Experimental mathematics is cool, but I don't get how this is that. Although he rails against symbolic manipulator programs as "pencils on steroids" so maybe Maple *doesn't* do that? In which case I guess these "theorems" are really just a bunch of utility function calls that say yes or no to a particular case, not prove a general conjecture?
posted by DU at 10:33 AM on February 18

I think this misses the point. The purpose of teaching geometry is to develop the problem solving skills of the students. Expressing the proofs in pseudo-code doesn't help the students grok this stuff; it only makes it more difficult.

Now, geometry is obviously useful outside of it being a learning exercise. Perhaps this approach would be useful in proving new theorems. But I doubt it's going to catch on in the classroom.
posted by cseibert at 10:36 AM on February 18

I love the smell of non-euclidean geometry in the morning.
...it's the smell of R'lyeh?
posted by juv3nal at 10:39 AM on February 18 [2 favorites]

Are there not three results to his proofs? True, false, and waiting for an answer to return? This seems to fly in the face of Godel and the Halting problem.
posted by FireSpy at 11:04 AM on February 18 [2 favorites]

takes off arthur koestler t-shirt
posted by clavdivs at 11:30 AM on February 18

This is why I am a designer, not a developer.
posted by Guy_Inamonkeysuit at 11:35 AM on February 18

I would be interested in reading a book about a non-insane version of this, where "this" means either experimental mathematics or algorithmic proofs. Recommendations?
posted by DU at 12:09 PM on February 18

In case people missed this:

All the theorems in this textbook were automatically discovered (and of course proved) by computer. The discovery program started with 3 generic points in the plane, and iteratively constructed new points, lines, and circles using a few primitives. Whenever a new point (or line, or circle, or whatever) coincided with an old one, a "theorem" was born. Then a search in Eric's Math Treasure Trove, version 1998, was performed, to see which of the theorems that were discovered by the Discovery Program were anticipated by humans; the program then automatically attached the human names to the theorems. Not surprisingly, all the theorems that turned out to be anticipated by humans, and that are presented in this very elementary textbook, were of very low complexity and depth.

So, he went backward; rather than, for example, symbolically proving known theorems via looking at their systems of linear equations or whatever, he "grew" random, known true ones. It's not that you should run these as code; they are the result of code which has already run.
posted by blenderfish at 12:47 PM on February 18 [2 favorites]

http://scienceworld.wolfram.com/biography/Zeilberger.html
Zeilberger, Doron (1950-)
Israeli-American mathematician who has made important contributions to the fields of hypergeometric summation and q-Series. The so-called Wilf-Zeilberger pair and Zeilberger's algorithm are indispensable tools for summing hypergeometric series, and these techniques are used extensively in modern computer algebra software. Zeilberger was also the first to prove the elusive result in combinatorial theory known as the alternating sign matrix conjecture, as well as a number of related propositions. Zeilberger was a co-recipient of the 1998 Steele Prize of the American Mathematical Society for his research on hypergeometric summation.
posted by metaplectic at 1:48 PM on February 18

http://www.math.rutgers.edu/~zeilberg/teaching.html

Experimental Mathematics: Combinatorial Statistical Mechanics
Experimental Mathematics: Automated (Symbolic!) Enumeration
Experimental Mathematics: Wilf-Zeilberger Algorithmic Proof Theory
Experimental Mathematics: Bioinformatics
Experimental Mathematics: Foundations
posted by metaplectic at 1:54 PM on February 18

So what's the significance of Shalosh B. Ekhad XIV ? 3-B-1-14?
posted by psyche7 at 2:12 PM on February 18

I just wanted to take this opportunity to mention that I love John Conway to death.
posted by cortex at 2:16 PM on February 18

Four Colors Suffice: How The Map Problem Was Solved

IIRC a lot of mathematicians took issue with the computer-aided proof of the 4 colors theorem... I wonder if that's still the case
posted by jcruelty at 2:28 PM on February 18

JOHN CONWAY 4 LIFE, eh?
posted by Pronoiac at 2:29 PM on February 18

DU, for a biased view of algorithmic proofs from the computer science field, a more established term for us is "constructive proof" (though that tends to imply the reasoning is carried out within one of the many constructive mathematics frameworks, which always causes some grumbling from the people who do it in classical frameworks; I think these last people tend to prefer to talk about the "computational content of proofs"). I'm afraid most of this work is in the shape of papers only, pehaps the manuals for provers such as Coq or NuPRL could make for some interesting browsing?

blenderfish, thanks for the heads-up. So he's using Maple programs in the sense others use typed lambda terms to represent proofs ("proof objects"), it's just his proof finding method that is a bit unorthodox and more in line with the experimental mathematics approach. I think now I get it, then, and gladly admit it's interesting. It reminds me of old ideas in machine learning and artificial intelligence for knowledge discovery. As others have mentioned, he might benefit from moving from Maple to some descendant of Prolog, too.
posted by Iosephus at 2:39 PM on February 18 [1 favorite]

FWIW, I think it goes "forward" too (i.e., Maple can do a bunch of symbolic mojo to prove these statements always evaluate to 'true',) but that's less interesting, IMO.
posted by blenderfish at 2:43 PM on February 18

I love the smell of non-euclidean geometry in the morning.
...it's the smell of R'lyeh?

The many-angled ones lurk at the bottom of the Mandelbrot set.
posted by Electric Dragon at 3:18 PM on February 18 [1 favorite]

Yeah, Maple's symbolic, not numerical. Assuming Maple does symbolic logic correctly (*) then I think these qualify as proper proofs. So not crazy afterall. (*) Maple execution is now part of your proof system you have to check for correctness. I assume that's the appeal to 2050, where we've already done all that testing and believe Maple and its execution hardware is correct.

Are there not three results to his proofs? True, false, and waiting for an answer to return? This seems to fly in the face of Godel and the Halting problem.

Nope, I'm imagining every demonstration proof on the web site either returns true or false in pretty short finite time. Godel/Halting says that there exist some theorems/machines for which there is no proof/answer. It doesn't say whether there are any unprovable theorems or non-halting machines that you actually care about.
posted by Nelson at 3:23 PM on February 18

I thought I was a nerd?
posted by winks007 at 7:08 PM on February 18

psyche7:

JG: Tell me about your frequent co-author Shalosh B. Ekhad

DZ: It is a charming individual. Of course it is made of silicon, and it is not really ONE body, but it is definitely ONE soul (software). The body has just been reincarnated many time. As we know, computers are very powerful, but their life expectancy is much shorter than that of humans, since computers get better and faster so quickly, you have to get a new one every three years, but you can always upload all the software from one Shalosh to the next, thereby guaranteeing the immortality of its soul.

JG: Where did you get that particular name?

DZ: The original Shalosh B. Ekhad was actually a Hebrew translation of the first PC that I owed, called AT&T 3B1. At the time it was a very innovative machine, the first UNIX PC, that was manufactured by AT&T in the 80s. The Hebrew translation of 3B1 is Shalosh B. Ekhad.
posted by parudox at 8:04 PM on February 18

I love the smell of non-euclidean geometry in the morning.
...it's the smell of R'lyeh?

The many-angled ones lurk at the bottom of the Mandelbrot set.

And the 6 dimensional kind will lead you to the Number of the Beast.
posted by scalefree at 8:38 PM on February 18

Why does the web of 2050 looks so much like the web of 1995?
posted by designbot at 9:17 AM on February 19

Why does the web of 2050 looks so much like the web of 1995?

Because, in the future, they've abolished all Web Designers.
posted by blenderfish at 11:13 AM on February 20