Follow Slashdot stories on Twitter

 



Forgot your password?
typodupeerror
×

Chinese Mathematicians Prove Poincare Conjecture 288

Joe Lau writes to mention a story running on the Xinhua News Agency site, reporting a proof for the Poincare Conjecture in an upcoming edition of the Asian Journal of Mathematics. From the article: "A Columbia professor Richard Hamilton and a Russian mathematician Grigori Perelman have laid foundation on the latest endeavors made by the two Chinese. Prof. Hamilton completed the majority of the program and the geometrization conjecture. Yang, member of the Chinese Academy of Sciences, said in an interview with Xinhua, 'All the American, Russian and Chinese mathematicians have made indispensable contribution to the complete proof.'"
This discussion has been archived. No new comments can be posted.

Chinese Mathematicians Prove Poincare Conjecture

Comments Filter:
  • by The Bungi ( 221687 ) <thebungi@gmail.com> on Monday June 05, 2006 @04:37AM (#15470770) Homepage
    I looked at TFA, and I was kind of lost after reading this:

    In its original form, the Poincaré conjecture states that every simply connected closed three-manifold is homeomorphic to the three-sphere (in a topologist's sense) S^3, where a three-sphere is simply a generalization of the usual sphere to one dimension higher.

    Homeomorphic. Thank god, they dumb it down a bit later:

    More colloquially, the conjecture says that the three-sphere is the only type of bounded three-dimensional space possible that contains no holes. This conjecture was first proposed in 1904 by H. Poincaré Eric Weisstein's World of Biography (Poincaré 1953, pp. 486 and 498), and subsequently generalized to the conjecture that every compact n-manifold is homotopy-equivalent to the n-sphere if it is homeomorphic to the n-sphere. The generalized statement reduces to the original conjecture for n==3.

    More colloquially, it's homotopy-equivalent to the n-sphere! Of course!

    Slow news day?

    • by joe 155 ( 937621 ) on Monday June 05, 2006 @04:40AM (#15470778) Journal
      Slow news day?

      this is actually quite a discovery; it's one of these things which has been hanging around for over a hundred years and it's good to finally have a proof... it's a little like proving P=NP... but a little less grand
      • by Barraketh ( 630764 ) on Monday June 05, 2006 @05:14AM (#15470872)
        Technically, it's more like proving P != NP, since that's the current accepted belief. Proving P=NP would be huge - this would give polynomial time algorithms for Travelling Salesman Problem, Boolean Satisiability Problem, and a slew of others (that all reduce to each other in polynomial time). Proving P != NP pretty much confirms what everyone believes to be true, similar to how the Poincaire conjecture was generally accepted to be true. Still, this is a major result, and clearly falls under the "News for nerds, stuff that matters" heading.
        • by Anonymous Coward on Monday June 05, 2006 @05:44AM (#15470943)
          Proving that P==NP wouldn't automatically give us polynomial time algorithms for any NP problem. The proof need not be constructive, and if it's not, it doesn't give algorithms. Granted, it seems easier to prove that P==NP by accidentally finding a polynomial time algorithm for an NP problem than otherwise, but don't assume that the prove would sove anything practical.
          • by IWannaBeAnAC ( 653701 ) on Monday June 05, 2006 @10:33AM (#15472155)
            That isn't quite true: you only need a polynomial time algorithm for a single NP-complete problem, and you can transform that into a polynomial time for all NP-complete problems.

            True, that if there was a non-constructive proof that P==NP, it might not be obvious what the polynomial time algorithm actually is. But since such a scenario would be probably the most astounding open problem in the history of mathematics, I don't think it would be an open problem for long ;)

        • echnically, it's more like proving P != NP, since that's the current accepted belief. Proving P=NP would be huge - this would give polynomial time algorithms for Travelling Salesman Problem, Boolean Satisiability Problem, and a slew of others (that all reduce to each other in polynomial time).

          Proving P=NP would cause doors to the Cthulhu dimention opened, as was shown by Charlse Stross [wikipedia.org] in The Atrocity Archives [wikipedia.org]

        • Though proving P != NP does not necessarily give any insight to heuristics for NP problems. The fact, in and of itself, has no value in engineering. But it would be a significant proof and highly newsworthy. Since both the P vs NP problem and the Poincare conjecture are pesky and hard problems that have received attention in the popular press, I would imagine, like you, it is worthy of mentioning on slashdot -- indeed if it wasn't mentioned here, slashdot would be suspect.
    • by Umbral Blot ( 737704 ) on Monday June 05, 2006 @04:51AM (#15470808) Homepage
      You might think that this is useless to you. However simply memorize those quotes and you can be prepared for any situation. Boss unexpectedly wants a status report? Sure boss, currently my I'm developong a compact n-manifold that is homotopy-equivalent to the n-sphere if it is homeomorphic to the n-sphere. We'll be done in a couple of weeks. Wife bothering you to take out the trash? Sure honey right after I demonstrate that every simply connected closed three-manifold is homeomorphic to the three-sphere (in a topologist's sense) S^3, where a three-sphere is simply a generalization of the usual sphere to one dimension higher. Never be at a loss for words again!
      • You might think that this is useless to you. However simply memorize those quotes and you can be prepared for any situation.

        My Boss replies with a frown and an "Are you bullshitting me?" to anything he can't understand.

        The consequences of trying to pull a fast one like this on the missus are too gruesome to detail here.
        • My Boss replies with a frown and an "Are you bullshitting me?" to anything he can't understand.

          Well, at least that's easy. You just say 'Of course not, Boss... how on Earth did you get that idea?' - with a perfectly straight face, of course.

          It's not that hard; look at all the moron politicians doing it on a daily basis, and professionally, too.

    • A translation... (Score:5, Informative)

      by FhnuZoag ( 875558 ) on Monday June 05, 2006 @06:02AM (#15470994)
      First, think in Four Dimensions. Not in terms of time, or something, but as a fourth spacial dimension - like in terms of up down, left right, in out, and foo bar. A 3 sphere is a sphere in that sort of space. For example, in three dimensions, a 2-sphere is just a normal sphere - a group of points that are all the same distance from a certain centre point. A 3-sphere in 4 dimensions is just the set of points in four dimensional space that are the same 'distance' from a point in 4D. (We define distance using the pythagorus formula sqrt(x^2 + y^2 + z^2 + k^2).)

      A 3-manifold is another four dimensional object - in fact, a class of objects. They are the analogies of surfaces in 3D space, only again we have it in 4D space. The 3-sphere, for example is an example of a 3-manifold. Simple, connected and closed are two topological properties describing what a surface is like. In layman's terms, simple connected and close means that the surface is well... just an obvious surface. The simple-connected-closed-3-manifold taken together essentially rule out the bizzare sorts of objects that mathematicians come up with. There won't be any 'holes' in the object, and there won't be any non-solid boundaries, the object can't go through itself, and you can't take two seperate objects and pretend the pair is a single one.

      So what does the conjecture say? It says that if we have any 3-manifold satisfying certain properties, there is way of distorting it (that's basically what homeomorphism means. Like you take the object as a piece of putty and stretch and pull it, or fold it, or whatever without cutting or gluing bits together) to make it into a 3-sphere.

      It's a sort of bubblegum theorem. You can chew up the manifold and blow it into a bubble. (Okay, it's not really like that, topologists.... But it's close enough)
      • by 140Mandak262Jamuna ( 970587 ) on Monday June 05, 2006 @09:22AM (#15471702) Journal
        ... who would pour their coffee into their doughnuts and dunk their cups in the soggy mess and look surprised. They are topologists. They cant tell a cup from a doughnut. When they need a ball in a hurry they will break off the handle of their coffee cup and try to bounce it on the court. These topologists are the most confused/confusing mathematicians around. ;-) They could make their math easier for us lesser mortals to understand. But they would rather knot.

      • by OldManAndTheC++ ( 723450 ) on Monday June 05, 2006 @12:19PM (#15473086)
        You lost me after 'First,'
      • Re:A translation... (Score:5, Informative)

        by AxelBoldt ( 1490 ) on Monday June 05, 2006 @01:01PM (#15473416) Homepage
        This is a really nice description of the theorem. I have just two small additions:

        simple connected and close means that the surface is well... just an obvious surface
        Simply connected means "no holes that you could capture with a loop". For instance, an ordinary sphere (what mathematicians call a 2-sphere, the surface of a ball) is simply connected: if you have any closed loop on the sphere, you can shrink it to a single point without leaving the sphere. The same is true for the 3-sphere. With a torus (surface of a donut) you can't always do that: there are certain loops that you can never shrink to a point without leaving the donut's surface. So the torus is not simply connected.

        A closed surface is one that does not allow points to go off to infinity (technical term: compact) and has no boundary. So for instance all of three-space is a nice simply connected 3-dimensional manifold, but it is not closed because points can run off to infinity. It also doesn't have a boundary. How could something without a boundary keep points from moving to infinity? Well, consider the 2-sphere, torus, or 3-sphere. No points in these spaces can shoot to infinity, but yet they don't have a boundary (a boundary point is a point where the surface abruptly stops). Closed manifolds somehow have to fold back on themselves.

        that's basically what homeomorphism means. Like you take the object as a piece of putty and stretch and pull it, or fold it, or whatever without cutting or gluing bits together
        Not quite: in additions to stretching and pulling, a homeomorphism also allows cutting and gluing, as long as you first cut, then move and stretch, and then glue together in exactly the same way that you cut earlier. So for example, take a little cylinder made from paper (without its top and bottom, just the side). Now cut it open along a straight line from top to bottom: if you unwrap it, you'll have a rectangle. Now create a double twist in that rectangle and glue it together along the same line again. The result is a terribly twisted "cylinder", and it is homeomorphic to the cylinder you started out with. (Had you made only a single twist rather than a double twist, then you wouldn't have glued points together that were earlier cut apart, and the result wouldn't have been homeomorphic to the cylinder--it would have been a Moebius strip.)
  • This is... (Score:5, Interesting)

    by mlow82 ( 889294 ) on Monday June 05, 2006 @04:45AM (#15470788)
    This is one of the Millennium Prize problems [wikipedia.org]! One down, seven more to go!
  • Ok, in plain english (Score:3, Interesting)

    by AuMatar ( 183847 ) on Monday June 05, 2006 @04:46AM (#15470793)
    Can someone boil down what the Poincare Conjecture is for us? I've had up to linear algebra in college, but I don't understand what itsa saying.

    Bonus points if you can explain some consequences of it being proven true.
    • by binarybum ( 468664 ) on Monday June 05, 2006 @04:55AM (#15470823) Homepage
      I think it basically has something to do with:

          If poincare conjecture = proved , my homepage switches to harsh new look. QED.
    • I didn't know what it was either but Wikipedia does have some simple descriptions which I'll try to summarise.

      In a nutshell, and assuming I've understood it, if you just consider a normal sphere, then it has a 2D surface. That surface is "simply connected" which appears to mean that if you take any two points on the surface and join them, then you can (smoothly) transform that joining "curve" into any of the other possible joins between those chosen points. Basically, there are no holes.

      If you then go
      • Not quite. The fact that the n-sphere is simply connected is pretty easy to prove. Poincare asked whether every closed simply connected 3-manifold is a 3-sphere. A surface is a 2-manifold. The sphere, plane, Mobius strip, Klein bottle, and so on are all 2-manifolds. A 3-manifold is just a natural extension of that idea, except instead of a surface, you have a 3-dimensional object. They're a bit hard to visualize, since most of them don't "fit into" our notion of space, in the same way that a sphere doesn
    • by Stalyn ( 662 ) on Monday June 05, 2006 @05:21AM (#15470890) Homepage Journal
      In topology spheres are identical to cubes and pyramids. However spheres are not identical to doughnuts. What PC says is that spheres are the only class of objects that are not doughnut-like (has holes). This seems trivial and obvious to most of us however to prove it is really hard. What it shows is that there is something fundamental and important about the sphere-like class of objects. It also says something important about space itself.
      • by david.given ( 6740 ) <dg@cowlark.com> on Monday June 05, 2006 @05:56AM (#15470980) Homepage Journal
        In topology spheres are identical to cubes and pyramids.

        A topologist is someone who doesn't know whether to dip their doughnut into their coffee mug, or vice versa...

      • Unfortunately this is wrong. A three-manifold is LIKE a sphere but in four dimensions. A sphere is a three-dimensional object with a two dimensional surface. A three-manifold is a four-dimensional object with a three dimensional surface. I suppose one way to visualize it is by taking our (three-dimensional) universe and imagining that if you traveled far enough in any direction you'd eventually end up back where you started, just like if an ant started walking in a straight line on the (two-dimensional) sur
    • From Millennium Prize Problems [wikipedia.org]

      In topology, a sphere with a two-dimensional surface is essentially characterized by the fact that it is simply connected [wikipedia.org]. The Poincaré conjecture is that this is also true for spheres with three-dimensional surfaces. The question has been solved for all dimensions above three. Solving it for three is central to the problem of classifying 3-manifolds.

    • by mozu ( 862682 ) on Monday June 05, 2006 @05:52AM (#15470967)

      Seems like whats been proven is that a doughnut != sphere.

  • more info (Score:3, Interesting)

    by airbie ( 767806 ) on Monday June 05, 2006 @04:46AM (#15470798) Homepage Journal
    More on the Poincare Conjecture: http://en.wikipedia.org/wiki/Poincar%C3%A9_conject ure [wikipedia.org]
  • by hyeh ( 89792 ) on Monday June 05, 2006 @04:49AM (#15470802) Homepage
    Wow, Chinese people solved a math problem?

    This is news?

    (j/k... I am Chinese).
    • NO the news is that the lest of the wold undestan wen thee Chinese peopre EXPRAIN the sorusion to the plobrem.

      *ducks*
    • by Anonymous Coward
      There are so many Chinese, some of them are bound to be good at math.
    • by 808140 ( 808140 ) on Monday June 05, 2006 @07:43PM (#15476525)
      As someone who has lived in China for a long time and was formerly a mathematician, I think that your statement is sort of ridiculous. For one thing, as others have pointed out, saying "some race is good at math" as if being good at math were something in your blood is silly. Having said that, the Chinese (as in, those from China) are, unfortunately, overwelmingly bad at Math. In ancient times the Chinese innovated quite competitively but this hasn't been true for a long time. Since I just took issue with your equating mathematical ability with racial characteristics, you can probably guess that there's another reason, and as it happens, I am prepared to qualify my statements.

      The Chinese school system (and in ancient times, the scholar system, which stratified society into a "scholar class" and the "masses") is completely and utterly innovation stifling. It emphasises testing and memorization above all else, and curiosity and individuality are systematically beaten out of students. No snide comments about communism, please, it has nothing to do with that (any mathematician will tell you that the Soviet Union produced a metric tonne of talented mathematicians, my advisor was one). Chinese students memorize everything. Because I speak Chinese and love math, I have tutored quite a number of high school and university undergraduate students in math and the simple reason that they suck at it is they basically cannot wrap their head around proofs.

      Proofs are difficult for most people at first, but you have to understand that the way a typical mainland Chinese kid approaches math is by memorizing every formula in his math textbook and then trying as best he can to choose the one that "works" with the problem he is presented. He does not do this because he stupid: he does this because the Chinese standardized testing system reinforces the behaviour. The exam problems are expressly designed so that various formulas are the "keys" to the problem, that is, answering the (usually multiple choice) question correctly relies on your ability to quickly recall one formula (perhaps two) and plug the numbers in effectively. So many problems are presented and so little time is given that no time for derivation or logic is really provided. Because of this, essentially every Chinese kid can recite from memory a whole host of trigonometric identities without having the faintest idea why they work or how to derive them, even when the derivation is relatively simple.

      Because there's so much anti-Chinese sentiment in the west these days and on Slashdot in particular, I want to reiterate for a moment and say that this is not an inherent failure in the Chinese kids themselves -- they are not stupid -- but they are completely crippled by their education system. From day one they memorize everything. They memorize entire passages written in old Chinese and are asked to reproduced them from memory at exam time -- I've been told by several kids here in Beijing that writing even one character wrong is essentially equivalent to forfeiting the entire problem. These are not 3 line passages folks: we're talking two or three pages of old Chinese. Imagine being told at 17 to memorize 3 pages of Beowulf. That's what we're talking about.

      The thing is (as any drama major will tell you) memorization, like all things, gets easier with practice. And from day one (when I first arrived in China I moonlighted as a Kindergarten teacher, so I have some first hand experience here) kids are memorizing stuff, from poems to proverbs to Chinese characters. It becomes easy for them, and over the years they depend on it more and more. The worst part is, high school and lower division level mathematics (if it can be called that) presents problems (like doing integrals or calculating derivatives) that lend themselves well to the "memorize a formula" method. And so Chinese kids tend to do exceptionally well in these courses, and then mistakenly assume they are good at math. This is in fact not
  • by Stalyn ( 662 ) on Monday June 05, 2006 @04:49AM (#15470804) Homepage Journal
    I thought the general consesus was that Perelman had proved Thurston's geometrization conjecture. If this proof by Zhu Xiping and Cao Huaidong is correct it must be a rephrasing of Perelman's work. Perelman is credited with making the major theoretical advances in order for any such proof. Basically he did most of the heavy lifting while these Chinese mathematicians basically dotted the i's and crossed the t's.

    The proof is 300 pages but I would guess the majority of it is an overview of Perelman's extension of Hamiltion's Ricci Flow.
    • I can't see why Perelman would share the credit. If his results are right, he proved it first. A second proof is impressive (moreso if it contains anything particularly new), but until shown otherwise, Perelman was the first, so he gets all the marbles.
      • I can't see why Perelman would share the credit. If his results are right, he proved it first.

        You haven't "proved" something until you have written it down in a form in which it convinces at least other specialists in your field. The fact that nobody knows for certain "if his results are right" is tantamount to the statement that he hasn't proven it yet.

        So, I suggest a simple rule: whichever of the two proof attempts will be verified first by at least a dozen other mathematicians or by a mechanical device,
        • You haven't "proved" something until you have written it down in a form in which it convinces at least other specialists in your field.

          That assertion is simply untrue.

          Suppose (and this a deliberately perverse example), Fermat had secretly developed all the machinery for Wiles' proof of his Last Theorem, and gone on to prove it. None of his contemporaries could possibly understand it. But the theorem would've been proved, even if no-one knew it.

        • The fact that a proof is beyond comprehension of some mathematicians does not mean it is less of a proof.
    • not necessarily (Score:5, Insightful)

      by m874t232 ( 973431 ) on Monday June 05, 2006 @08:02AM (#15471296)
      The purpose of a proof is to communicate a sequence of statements such that each and every individual step is easily derivable from axioms or well-known theorems. Let me emphasize this again: a proof is about communication, not merely about making true statements.

      Perelman apparently failed to do this: he may have produced a sequence of true statements that could somehow form a subsequence of a complete proof, but he has apparently not supplied enough detail to demonstrate his point to even specialists in his area. The fact that he may have done "the heavy lifting" or that he may have provided the key ideas doesn't change that.

      I think it is valid to give all three mathematicians equal credit. And, strictly speaking, the people who actually have done the proof are the ones who "dotted the i's" because that's what ultimately constitutes a proof.
    • A collection of facts is no more a science than a heap of stones is a house.
      - Poincare

      Somehow I think Poincare would appreciate the complete proof.
  • This has not shown up in the mainstream Western press, which is very curious. A more believable article would be a report that Perelman's proof works.
  • Math isn't dead (Score:5, Interesting)

    by colin353 ( 964700 ) <colin353@gmaiREDHATl.com minus distro> on Monday June 05, 2006 @05:00AM (#15470841)
    This is another reason why math isn't dead. The world's problems aren't solved, and they aren't impossible, either.

    I was just having a conversation about this yesterday with my math teacher.

    Lots of people think that high level math is just advanced adding and subtracting.

    This is good stuff. Props to Zhu Xiping and Cao Huaidong- this shows people that a career in studying mathematics is actually an interesting and rewarding career.
    • by Anonymous Coward on Monday June 05, 2006 @05:57AM (#15470983)
      The problem is rather that the complexity of current math problems has approached the limit of what humans are able to handle. Any 8th grader can verify Pythagoras, but verifying a proof like the one at hand can only be done by a handful of the world's best mathematicians and may take weeks to complete (remember what happened when Wiles proved Fermat's Last Theorem). A proof is meant to demonstrate that a given conjecture is true by splitting it up into many small steps which are considered self-evident. However, today even verifying a proof is very hard and the time may be near when no one on earth will be able to handle the complexity of this task anymore, so that even if a proof is given it may be impossible to say with certainty whether it is valid. Computers may help here, but other problems arise in that context.
      • I don't really think that's true.

        On our undergraduate history of science class, one of our texts was Kuhn's book. His arguement was that science doesn't work by continually adding more stuff on top of what is already there but works in paradigms.

        So, for example quantum physics was a paradigm change. The photoelectric effect is explained by 7th graders but now higher level quantum mechanics cannot be. Every once is a while someone comes up with a total paradigm change on how problems are supposed to be a

        • The actual proof could be just 1 line if we assumed the Taniyama-Shimura conjecture to be true.

          You have no idea what "proof" means if you think you can prove something by assuming that one of the premises is true when that premise is neither an axiom or a theorem that has been previously proved.

          However, if you're right, I'd like 1 million dollars because I've just proved the Riemann hypothesis. My proof only requires that you assume the truth of the Spear Conjecture, which states that the Riemann Hypoth

          • And you apparently have no ability to read what the GP said. Specifically, he suggested that most of Wiles' effort was directed at proving the Taniyama-Shimura conjecture. From that point on, it was a simple step to prove Fermat's Last Theorem (for some extremely esoteric value of 'simple').

            Note this line here:

            Actually, Wiles proof of FLT is a simplification of the Taniyama-Shimura conjecture which he proved I believe.

            Whether the grandparent poster's assertion about this method is accurate

        • Your post was quite good, but the last paragraph is contradictory with the rest.

          A good mathematical proof is as self-contained as possible; that's probably an utopia, but a proof of Fermat's last theorem which is just that line you mentioned does no good whatsoever to anyone reading it. If a proof is self-contained (or almost), someone who reads it and understands it can then safely say that he/she understands WHY the theorem is true. Otherwise, he may well be relying on someone else's mistakes (adding more
      • by RackinFrackin ( 152232 ) on Monday June 05, 2006 @11:12AM (#15472436)
        However, today even verifying a proof is very hard

        While that's true of some proofs, it's certainly not true of all of them, or even most of them. Every year, hundreds of mathematics journals collectively publish thousands of new proofs. Some are more difficult to verify than others, but they are all verifiable (or falsifiable in the case of published errors).

        the time may be near when no one on earth will be able to handle the complexity of this task anymore

        I doubt we'll ever see that happen. Of course as a mathematical field matures, the number of accessible problems will approach zero and we're left with only the very difficult problems. However, new fields arise and give us a host of new problems to explore.
  • by distantbody ( 852269 ) on Monday June 05, 2006 @06:29AM (#15471065) Journal
    What are the useful applications of this? Can I get a quantum computer next week!?
  • by 2Bits ( 167227 ) on Monday June 05, 2006 @06:37AM (#15471085)
    I assert that there is a torrent of the proof somewhere on the net. Now can someone prove that, please?

  • by Anonymous Coward on Monday June 05, 2006 @07:14AM (#15471181)
    I'll accept the proof when it's been properly reviewed by peers. Just publishing a proof in a journal doesn't equate to a correct proof, now does it?
  • by advocate_one ( 662832 ) on Monday June 05, 2006 @07:16AM (#15471184)
    "isn't that like the Da Vinci Code???"

    I think it makes a good thriller title... "The Poincare Conjecture"
    • Re:Joe Public goes (Score:3, Interesting)

      by dido ( 9125 )

      There's a whole slew of mathematical theorems, conjectures, hypotheses, et. al. that sound like Robert Ludlum novels [everything2.com]:

      1. The Riemann Hypothesis
      2. The Eisenstein Criterion
      3. The Fredholm Alternative
      4. The Poincare Conjecture
      5. The Fourier Transform
  • Serious errors in mathematical papers are so common that I wouldn't put any trust in this until the proof has been around for a decade or two; even if Cao and Zhu did everything correctly, there's a good chance that something they relied on turns out not to be true after all.

    In the long run, mathematics really needs considerably more formality than it is using now, as well as mechanical support for the bookkeeping necessary for long and involved proofs. Actually, the tools already exist, it's just that wor
    • by Yrd ( 253300 ) on Monday June 05, 2006 @08:33AM (#15471433) Homepage
      This is something I'm peripherally involved in - automated proof tools are becoming more capable all the time, and I was at a keynote address by Tom Hales (University of Pittsburgh) who has been using such tools to formalise one of the proofs he's known for. There's some resistance (a lot, perhaps) to using such things in the mathematical community, but as a mathematician who's decided to use them rather than a computer scientist who's trying to prove that they're useful, he's hoping to change some minds and it's also nice for those of us in AR research to hear that there are mathematicians out there using them!

      Unfortunately, automated proof tools are not sophisticated enough to handle the kind of maths seen in solving the Really Big Problems. Not yet, anyway.

The means-and-ends moralists, or non-doers, always end up on their ends without any means. -- Saul Alinsky

Working...