Beta
×

Welcome to the Slashdot Beta site -- learn more here. Use the link in the footer or click here to return to the Classic version of Slashdot.

Thank you!

Before you choose to head back to the Classic look of the site, we'd appreciate it if you share your thoughts on the Beta; your feedback is what drives our ongoing development.

Beta is different and we value you taking the time to try it out. Please take a look at the changes we've made in Beta and  learn more about it. Thanks for reading, and for making the site better!

Achieving Mathematical Proofs Via Computers

timothy posted more than 5 years ago | from the send-picture-of-abacus dept.

Math 209

eldavojohn writes "A special issue of Notices of the American Mathematical Society (AMS) provides four beautiful articles illustrating formal proof by computation. PhysOrg has a simpler article on these assistant mathematical computer programs and states 'One long-term dream is to have formal proofs of all of the central theorems in mathematics. Thomas Hales, one of the authors writing in the Notices, says that such a collection of proofs would be akin to the sequencing of the mathematical genome.' You may recall a similar quest we discussed."

cancel ×

209 comments

Sorry! There are no comments related to the filter you selected.

unfortunately (-1, Flamebait)

Anonymous Coward | more than 5 years ago | (#25667115)

it will only prove that you're all a bunch of fucking nerds!!!

Wikipedia is for fucking bastards (-1, Flamebait)

Anonymous Coward | more than 5 years ago | (#25667157)

Don't donate to it let it go out of business for being deletionist bastards.

godelstheorem? (3, Insightful)

retchdog (1319261) | more than 5 years ago | (#25667165)

Why is this tagged "godelstheorem"? It's not like incompleteness magically applies only to electronic computers, as opposed to meatbags...

Re:godelstheorem? (5, Insightful)

QuantumG (50515) | more than 5 years ago | (#25667293)

I honestly think they need to stop teaching the halting problem to freshmen CS majors. They're just too inexperienced to understand that theory and practice are two different things.. so this whole "limits of computation" thing stifles their enthusiasm.

Re:godelstheorem? (5, Insightful)

AWhistler (597388) | more than 5 years ago | (#25667603)

Not only that, but people should stop using this as a crutch in general. The journey is worth the effort, even knowing that you can never reach the end. This is why I agreed with Godel, Escher, Bach by Hofstadter and disagreed with The Emporer's New Mind by Penrose.

One of Penrose's conclusions was that any attempt at artificial intelligence is necessarily incomplete, so it won't be possible, while Hofstadter said that it is possible to successively approximate something intelligent, and we can learn a LOT about ourselves in the attempts, and that in itself is worth it.

At least that is one of the many things I got from the two books.

Re:godelstheorem? (4, Insightful)

BitterOak (537666) | more than 5 years ago | (#25668121)

One of Penrose's conclusions was that any attempt at artificial intelligence is necessarily incomplete, so it won't be possible, while Hofstadter said that it is possible to successively approximate something intelligent, and we can learn a LOT about ourselves in the attempts, and that in itself is worth it.

Not only that, but Penrose doesn't offer any actual proof that AI is impossible, merely speculative reasoning. Therefore it seems doubly important that we continue our attempts to advance AI. Firstly, that the journey itself is worth the effort, and secondly we really need to find out for ourselves if it is possible.

Re:godelstheorem? (5, Informative)

kohaku (797652) | more than 5 years ago | (#25668879)

Why should AI be impossible? Surely it must be possible, with the human brain as evidence? One might argue that the brain is merely a biological computer not fully understood. Unless there is a "higher intelligence" giving humans beings thoughts, then AI must be possible. I suppose this is analogous to a Human "telling" a machine what to think, though, and gives rise to the "who created the creator" argument, but that's getting a little offtopic...
This comment is somewhat similar to one below [slashdot.org] for which I apologise, but I wanted to expand on the point slightly :)

Re:godelstheorem? (3, Interesting)

Eli Gottlieb (917758) | more than 5 years ago | (#25671503)

One might argue that the brain is merely a biological computer not fully understood.

Or, perhaps, humans could be nondeterministic and therefore not computers at all.

Re:godelstheorem? (1)

Estanislao Martínez (203477) | more than 5 years ago | (#25671615)

One might argue that the brain is merely a biological computer not fully understood.

  1. How would that be an argument, and not just an analogy?
  2. One might argue that my bedroom walls are a physical computer not fully understood, simply by stating some structural correspondences between it and some Turing machine. Where does that leave arguments to the effect that "the brain is a computer"?

Re:godelstheorem? (0)

Anonymous Coward | more than 5 years ago | (#25670035)

As a scientist, Penrose offers no proof because you can't prove a negative.

Re:godelstheorem? (4, Insightful)

Sparr0 (451780) | more than 5 years ago | (#25670207)

Of course you can prove a negative, usually by contradiction. Assume the opposite and see if that produces a contradiction. If it does, then the original negative is true.

Re:godelstheorem? (1, Insightful)

Anonymous Coward | more than 5 years ago | (#25668541)

Isn't non-artificial intelligence necessarily incomplete as well? It's not like the brain has a sprinkling of magic pixie dust that computers can never have.

Re:godelstheorem? (2, Interesting)

z-j-y (1056250) | more than 5 years ago | (#25668681)

can human brain be simulated by a Turing machine? It's plausible that human brain obey physics - but is physics Turing computable?

Of course we can create physical machines that's the same as human brains - million of of them everyday:)

Re:godelstheorem? (1)

AWhistler (597388) | more than 5 years ago | (#25668687)

That *is* one of the corollaries I took away from the two books as well.

Re:godelstheorem? (0)

Anonymous Coward | more than 5 years ago | (#25668871)

I thought Penrose did essentially think the human brain had some unknown "magic" ingredient that non-human intelligence could never have?

Re:godelstheorem? (1)

retchdog (1319261) | more than 5 years ago | (#25670985)

Yeah, quantum mechanical fluctuations in the microtubules.

No one really takes this seriously, not to mention that we do have computers which are affected by quantum mechanics.

Re:godelstheorem? (4, Insightful)

Draek (916851) | more than 5 years ago | (#25669113)

One of Penrose's conclusions was that any attempt at artificial intelligence is necessarily incomplete, so it won't be possible

But wouldn't Godel's theorem imply that it'd be impossible to build a flawless, all-encompasing intelligence, not necessarily an imperfect one? fsck, even I as a human (allegedly the "superior" intelligence) sometimes feel that my decisions are based solely on the output of a Random() call in my brain rather than logical thought, no reason why a machine has to be different.

AI isn't about trying to build God, it's just about something that can learn new stuff, or at least that's my take of it.

Re:godelstheorem? (1)

Kagura (843695) | more than 5 years ago | (#25669355)

AI isn't about trying to build God ...

I hope we reach the singularity in my lifetime. But considering the state of AI at this point in time, I will be long dead before immortality arrives.

Re:godelstheorem? (5, Insightful)

jonaskoelker (922170) | more than 5 years ago | (#25669757)

But wouldn't Godel's theorem imply that it'd be impossible to build a flawless, all-encompasing intelligence, not necessarily an imperfect one?

Gödel's theorem's concludes, simplified a bit, that it's impossible to know the truth, the whole truth and nothing but the truth about sufficiently complex math. In this context, sufficiently complex means "anything that includes addition and multiplication of natural numbers".

An AI may be able to prove that sum(range(1, n+1)) == n*(n+1)//2 for all natural numbers n; that is, it may output a string that's a valid proof. Smart ones can, dumb ones can't. Just like humans. Intelligence is what limits you.

But if a set of axioms and inference rules don't allow for a proof of a given theorem T, no matter how smart you are, even if your silicon brain is smarter than all of mankind, monkeykind and birdkind added up, you can't transcend any limitation that's found wholly outside your intelligence. As in this case, where it's the nature of the mathematics you've made that prevents T from being proven, and not your inability to find the proof.

Similarly, if we agree that no evidence or reasoning can prove or disprove the existence of god, then no AI can know whether god exists: it's not your knowledge or ability to reason that limits you, it's the nature of knowledge and reasoning itself.

Looked upon that way, Gödel's theorem doesn't say anything about AI. It says something about the world.

I don't know what a "perfect" intelligence is. One that can solve all NP problems in O(1) time and space? Or s/NP/Recursive/? Or just something that can solve all recursive problems in finite time? To implement that, all we lack is the ability to store unbounded information in a world of finitely many atoms. Can intelligence do something more than Turing machines? Does that mean the answer is no? Or that we need to connect nerves to the PCI bus?

Re:godelstheorem? (1)

Draek (916851) | more than 5 years ago | (#25670093)

Exactly. Now, my question is, is an AI required to answer such questions? is an AI even required to be able to add two numbers? Godel's theorem as I understand it essentially states that any system (in this case, our AI), when faced with some questions, will either ignore the answer or give an answer that contradicts itself, but is that a problem?

As you say, Godel's theorem says more about the world than it does about intelligences per se, and if not being able to prove or disprove a specific statement means our AI isn't intelligent, by Godel's theorem nothing can be, not even us.

I don't know what a "perfect" intelligence is. One that can solve all NP problems in O(1) time and space? Or s/NP/Recursive/? Or just something that can solve all recursive problems in finite time?

I was thinking more like a religious God: an intelligence that knows anything and everything in all possible ways that they can be known. But is that the minimum for an AI? I'd be happy with a virtual pet that eats, poops, and barks at strangers without being programmed to know what it means to eat, poop, bark, or what's a stranger. No need to demonstrate long-standing mathematical problems or even do my children's math homework.

Just make it stop (0)

Anonymous Coward | more than 5 years ago | (#25670775)

The question of whether or not God exists is pure sophistry. A sufficiently intelligent agent would pay it no more heed than the question, "Do concepts live in barns?"

Similarly, Godel's theorems are often portrayed in sophist manner. They prove interesting and perhaps surprising facts about mathematics, but they don't say anything remotely close to "some truth is unknowable".

Re:godelstheorem? (1)

jonaskoelker (922170) | more than 5 years ago | (#25669779)

my decisions are based solely on the output of a Random() call in my brain rather than logical thought, no reason why a machine has to be different.

It's not random, it's just that every ten seconds you get a hard disk and feel like doing an integrity check.

No reason why a machine has to be different. [zomfg, I just googled "mecha porn". Rule 34 works, biatches].

Re:godelstheorem? (1)

not-my-real-name (193518) | more than 5 years ago | (#25669255)

One of Penrose's conclusions was that any attempt at artificial intelligence is necessarily incomplete, so it won't be possible, while Hofstadter said that it is possible to successively approximate something intelligent, and we can learn a LOT about ourselves in the attempts, and that in itself is worth it.

It seems to me that unless there is something supernatural involved (a soul), it should be possible to construct an artificial intelligence. It may be something different than a computer, but it should be possible. The rest is just engineering.

Re:godelstheorem? (1)

retchdog (1319261) | more than 5 years ago | (#25670945)

I heard that the Fields medalist Michael Freedman was trying to prove P!=NP, by reducing the problem to a corollary of Godel's result (the idea being to construct a mapping from NP-problems to "true statements", such that P-problems wind up in the subset of "provable statements").

The notion of using the biggest "negative" result in mathematics to solve one of the most elusive problems is truly inspiring.

I don't know if it'll work though, and I haven't heard much since a few years ago. I've long since given up on pure mathematics myself.

Re:godelstheorem? (1)

Chris Burke (6130) | more than 5 years ago | (#25668061)

I honestly think they need to stop teaching the halting problem to freshmen CS majors. They're just too inexperienced to understand that theory and practice are two different things.. so this whole "limits of computation" thing stifles their enthusiasm.

I suppose. Personally I find it very useful in explaining why, generally speaking, the only way to really know how a program will respond to certain inputs is to test it. Theory and practice are not all that far apart. In theory, the halting problem only states that there is no algorithm that can answer the halting question for all programs and inputs, given infinite resources and potentially infinite running time. In practice, no such algorithm exists for most programs and inputs on real machines.

It may stifle their enthusiasm, but it will at least explain why, for example, the only real way to test the control logic for your microprocessor is by writing lots and lots of tests and checking their output. I know that when I entered school I was hoping there was a "magical" (as in unknown to me) method of writing correct programs other than my previous hack->run->debug cycle, but the reality is that formal verification is only practical for a small subset of problems.

Re:godelstheorem? (1)

GodKingAmit (1192629) | more than 5 years ago | (#25668261)

So far.

Re:godelstheorem? (1)

InfiniteLoopCounter (1355173) | more than 5 years ago | (#25671191)

In theory, the halting problem only states that there is no algorithm that can answer the halting question for all programs and inputs, given infinite resources and potentially infinite running time. In practice, no such algorithm exists for most programs and inputs on real machines.

It may stifle their enthusiasm, but it will at least explain why, for example, the only real way to test the control logic for your microprocessor is by writing lots and lots of tests and checking their output.

It may stifle enthusiasm a little, but it does get one thinking about such things.

As I understand it from CS lectures, the halting problem can be briefly summarized by the following argument:

- Assume there is a halting program.

- Now run the halting program on itself. There is no way to tell if it will halt or not, which is a contradiction. Therefore, such a program cannot exist in general.

Whilst it is a logical argument (the full argument being more mathematical), I don't like this very much. You have to be very specific in placing some restrictions on your problem space. Namely, you can't write an infinitely long code and there is only a finite number of possible inputs. These aspects seemed to me to be glossed over too much, especially the part about inputs which should lead to conditional halting.

Furthermore, what is to stop you from assessing your code as you are writing it? Why not just test every possible combination of inputs on the code as it is being generated (making the appropriate assumptions so that this does not actually check every combination of inputs)? Whilst not feasible in practice for all scenarios, shouldn't this be possible in theory. I also note that most of the time I spend coding is idle time for the processor.

Clever checking might then just check for two states where all the dynamic variables are the same (which would probably be easier in practice where methods only contain limited subsets of variables).

I am not knocking the logic of the halting problem, just how it is introduced as being this general statement that construction of such a program is theoretically impossible. Any human can tell whether or not the hello world programs which came before will halt or not halt after a casual glance. Why cannot a machine employ a simple finite state approach to yield a conditional solution (sometimes the actual answer maybe "unknown" in practice due to random numbers or any code which does not yield the same answer every time for the same inputs) for a possible-to-write program for which all the code is visible?

Well, that is the end of my rant. If I have got this the wrong way then please feel free to point out problems in my argument.

Re:godelstheorem? (1, Interesting)

Anonymous Coward | more than 5 years ago | (#25671435)

Let's take a step back and not worry about abstract reasoning for a moment. Here's a concrete example with a very simple function. You really should try to solve this before talking about using "clever checking", etc.

/* pseudocode: assume "int" is an infinite precision integer with no overflow */
int collatz_number (int n)
{
  int steps = 0;
  while (n > 1)
    {
      if ((n % 2) == 1) { n *= 3; n += 1; };
      n /= 2;
      steps += 1;
    }
  return steps;
}

(Hint: Nobody knows if it always halts or not. My apologies if you get hooked on this problem too...)

Re:godelstheorem? (2, Interesting)

InfiniteLoopCounter (1355173) | more than 5 years ago | (#25671555)

Again, restrict the problem space to what is feasible. This pathological example is one of infinite complexity that is impossible in practice (int cannot be substituted for an infinite precision integer). There will be overflow or there will be a state where n is the same as a state before after a finite number of steps (there are only a finite number of possible values for n). So this program will conditionally halt for different values of n (of which there is a finite number).

I was talking about applying theory to something that is possible. Obviously you can set up a simple system which is impossible to execute and generate an infinite space of inputs and outputs. This is plain cheating in reality, often the mistaken realm of application of the halting problem.

Re:godelstheorem? (0)

Anonymous Coward | more than 5 years ago | (#25671327)

Thye difference between theory and practice is greater in practice than it is in theory.

Re:godelstheorem? (2, Interesting)

Jane Q. Public (1010737) | more than 5 years ago | (#25667399)

Of course this applies. No, Gödel's theorem doesn't just apply to computers, but it does apply too!

And it is actually a very relevant point. Since Gödel proved that a formal system must be either incomplete or inconsistent -- and we do not really know which one applies to mathematics -- it may be that a "central" theorem of mathematics will contradict some other finding, later, which turns out to be equally central.

Not very likely, but who knows?

Re:godelstheorem? (2, Informative)

ComaVN (325750) | more than 5 years ago | (#25667465)

a formal system must be either incomplete or inconsistent -- and we do not really know which one applies to mathematics --

Except that we do, and it's incomplete.

Now, as to which applies to meatbags, my guess is they're both incomplete and inconsistent.

Re:godelstheorem? (1)

uncmathguy (936555) | more than 5 years ago | (#25668265)

>Except that we do, and it's incomplete.

Sorry if I missed the joke if your post was supposed to be ironic, but of course, we don't know that. In fact, Godel proved that it is not possible to prove that mathematics is consistent. And of course, if mathematics is not consistent, then it is trivially complete.

As for meatbags, I didn't realize such terms applied.

Re:godelstheorem? (1)

Jane Q. Public (1010737) | more than 5 years ago | (#25669793)

Really? We have a consistency proof? I would be interested in knowing more about that.

Re:godelstheorem? (4, Informative)

exp(pi*sqrt(163)) (613870) | more than 5 years ago | (#25667685)

We already know that a statement like the continuum hypothesis can be proved neither true nor false from ZFC. We don't need Godel's theorem to prove "incompleteness or inconsistency" when we have lots of practical examples of its incompleteness. So your claim of "don't know" is false.

First order logic is consistent and complete. In fact, Godel proved this. Additionally, consider the set S of all possible propositions of set theory. Somewhere in the power set of S must lie the set of all true propositions. Just take these as your axioms. Voila, a formal system that is both complete and consistent. Your characterization of Godel's theorem is incorrect.

Re:godelstheorem? (2, Insightful)

Jane Q. Public (1010737) | more than 5 years ago | (#25669967)

My understanding was that Gödel proved that S could not contain itself, which was the downfall of that very argument. Consider a statement about S: "S contains all possible propositions." That proposition may be true, but it is not possible to prove that proposition within S, so S is incomplete. Q.E.D.

That is a brief summary but even if I misunderstood that, a proven incompleteness by itself still does not prove consistency. They are not mutually exclusive.

Re:godelstheorem? (1)

exp(pi*sqrt(163)) (613870) | more than 5 years ago | (#25670905)

Propositions are very simple things. They're just strings of characters. You can easily write a computer program to generate all propositions and there's no problem working with the set of all propositions. Given any set, the set of all subsets exists. This is the Power Set Axiom [wikipedia.org] . This set contains every possible set of propositions, so it certainly contains the set of all true propositions.

An important part of Godel's incompleteness theorems that is often overlooked is that the set of axioms has to be recursively enumerable (r.e). In other words it has to be possible to write a computer program that lists the axioms, and no other propositions. My example fails because even though the set of all true propositions exists, it's not r.e. So it's not the kind of axiom set that Godel's theorems talk about. That's why these theorems can coexist with the example axiom set I talked about.

The other example I gave was first order logic. The incompleteness theorems don't talk about this either because you can't do arithmetic in first order logic. The theorems only apply to formal systems in which you can do arithmetic. Check out the wording at wikipedia [wikipedia.org] .

A consequence of the incompleteness theorems is that we can't write a program that systematically lists all true mathematical propositions. But that's *not* what the original article is about. It's about machines checking human-generated proofs, and maybe filling in details. Godel's incompleteness theorems provide no objection to this at all. In principle, checking human proofs is really easy, you just check the axiom or derivation step that was used at each step in the proof. It's an undergraduate programming exercise to do this. The problem is more human than logical: complete formal proofs of non-trivial results are very very long and so don't correspond to what mathematicians actually write.

Pardon me (1)

Jane Q. Public (1010737) | more than 5 years ago | (#25670875)

I meant "inconsistency and incompleteness are not mutually exclusive".

On the contrary, they often go hand-in-hand.

Re:godelstheorem? (0)

Anonymous Coward | more than 5 years ago | (#25671325)

Somewhere in the power set of S must lie the set of all true propositions. Just take these as your axioms. Voila, a formal system that is both complete and consistent.

Such a set is infinite. You want your set of axioms to be finite and you want to be able to enumerate all true propositions from it. Otherwise, we cannot use it.

Re:godelstheorem? (1)

hardburn (141468) | more than 5 years ago | (#25667925)

Since GÃdel proved that a formal system must be either incomplete or inconsistent . . .

There's a third possibility, which is "not powerful enough to be really interesting".

what is a central theorem? (4, Interesting)

Hatta (162192) | more than 5 years ago | (#25667187)

Godel of course proved that you can never have a complete list of all true statements in mathematics. So if they're just limiting it to "central" theorems, how do they decide what's central and what's not?

Re:what is a central theorem? (3, Interesting)

eldavojohn (898314) | more than 5 years ago | (#25667227)

Godel of course proved that you can never have a complete list of all true statements in mathematics. So if they're just limiting it to "central" theorems, how do they decide what's central and what's not?

Just because a list is incomplete doesn't make it any less useful, does it?

I'm certain Wikipedia, any of Google's search results & my list of liqueurs to pick up on the way home are all incomplete ... although they are all highly useful.

To answer your question, I would start with all the theorems that are the most employed/referenced by other theorems and work from there. Who knows what might turn up?

Re:what is a central theorem? (1)

networkBoy (774728) | more than 5 years ago | (#25669389)

I'm fairly sure this search [google.com] isn't very useful.
-nB

Re:what is a central theorem? (0)

selfdiscipline (317559) | more than 5 years ago | (#25671087)

But our current body of theorems biases us to look for theorems that are well connected with them.

How do we know that our mathematical knowledge isn't just a local maximum?

Re:what is a central theorem? (4, Interesting)

jfengel (409917) | more than 5 years ago | (#25667307)

TFA also says:

When it comes to central, well known results, the proofs are especially well checked and errors are eventually found. Nevertheless the history of mathematics has many stories about false results that went undetected for a long time.

In other words... maybe, just maybe, there's a hole in one of the theorems we use all the time, and an error would have severe ramifications. Or at the very least, there might be an opportunity lurking in an assumption we didn't realize we were making, like the way non-Euclidean geometry was just sitting there waiting to be discovered.

They're not really "limiting" it to central theorems, so they don't need a definition. But the more important (read, broadly-used) a theorem is, the more interesting it will be to have the proofs double-checked by a computer.

That computer proof may itself be wrong if the programmers are wrong, but as with the proofs we already have, it's just one more set of "eyes" looking for problems.

Re:what is a central theorem? (1, Interesting)

exp(pi*sqrt(163)) (613870) | more than 5 years ago | (#25667347)

> Godel of course proved that you can never have a complete list of all true statements in mathematics

It doesn't need Godel to figure out that you can't make a list of all possible true statements in mathematics. Given that even a child knows that there are an infinite number of true statements I can only think that you cite Godel in an attempt to give your trivial observation an exaggerated air of authority.

Re:what is a central theorem? (0)

Anonymous Coward | more than 5 years ago | (#25668683)

Lists can be (countably) infinite can't they?

Maybe the OP meant "list" colloquially, as in "set".

Re:what is a central theorem? (1)

Bromskloss (750445) | more than 5 years ago | (#25667397)

Godel of course proved that you can never have a complete list of all true statements in mathematics.

I didn't know that was what he really proved, but in any case, why do we have to bring up Godel every time it comes to automated proving? Godel surely doesn't forbid us to search for proofs of a given statement, or even search for new theorems, if we can (in some automated fashion) determine if they are interesting or not.

And how do I enter non-ASCII characters? >-(

Re:what is a central theorem? (1)

demi (17616) | more than 5 years ago | (#25667981)

Use the HTML entity for Gödel?

Re:what is a central theorem? (3, Informative)

melikamp (631205) | more than 5 years ago | (#25667407)

Godel of course proved that you can never have a complete list of all true statements in mathematics. So if they're just limiting it to "central" theorems, how do they decide what's central and what's not?

Godel proved that you can never have a complete and recursive list of axioms for arithmetic. Regardless, "central" in TFA means well-known, which, IMHO, is fair enough. Letting a computer know proofs of all major results seems to be a necessary step on the way to building a silicon mathematician.

Re:what is a central theorem? (4, Funny)

Bromskloss (750445) | more than 5 years ago | (#25667479)

on the way to building a silicon mathematician.

I think we have one at our department. He's, like, very stiff.

Re:what is a central theorem? (1)

TheVelvetFlamebait (986083) | more than 5 years ago | (#25669525)

That's why I've always preferred the silicone mathematician.

Re:what is a central theorem? (1)

melikamp (631205) | more than 5 years ago | (#25670919)

Oh my god, it's a word??

Re:what is a central theorem? (1)

florescent_beige (608235) | more than 5 years ago | (#25667511)

Godel proved that you can never have a complete and recursive list of axioms for arithmetic.

The Incompleteness Theorem:

For any consistent formal theory that proves basic arithmetical truths, an arithmetical statement that is true but not provable in the theory can be constructed. That is, any theory capable of expressing elementary arithmetic cannot be both consistent and complete.

What's this about recursive?

Re:what is a central theorem? (1)

Ann Coulter (614889) | more than 5 years ago | (#25667595)

The "elementary arithmetic" (Peano arithmetic) is recursive.

Re:what is a central theorem? (1)

melikamp (631205) | more than 5 years ago | (#25667801)

The set of all true statements of arithmetic does exit, but we cannot write a program that would reliably recognize true statements (i.e., always halt with a definite answer). We cannot even have a program that would recognize some set of axioms which we could use to derive all facts of arithmetic.

Re:what is a central theorem? (2, Interesting)

DamnStupidElf (649844) | more than 5 years ago | (#25667451)

It's no worse than standard mathematics done by humans. There's no indication that humans can present a proof of a theorem that says it has no proof (for instance, can you prove "this statement has no proof of its truth" is true or false or neither?), so humans are no more powerful than a formal system in which one can construct Godel's incompleteness proof.

Specifically, I'm sure that the "central" theorems they're referring to are ones nearest to set theory or some other basic set of axioms. It's much harder to prove Fermat's last theorem or the Poincare Conjecture with complete formalism than it is to prove simple theorems of arithmetic. Once the central theorems are proven, it is simpler to tackle more complex theorems using the already proven theorems as lemmas.

Re:what is a central theorem? (1)

fuzzyfuzzyfungus (1223518) | more than 5 years ago | (#25667817)

I strongly doubt that this is the case; but it would be philosophically fascinating if computerized mathematical proving were worse than the math done by humans. If it could be demonstrated that building a system that replicates what humans can do is impossible, rather than merely difficult, that would strongly suggest that human consciousness is Something Other.

I have no reason to believe that that is the case, and I am very strongly inclined to doubt it; but were it so, this might be one of the few places that you could actually demonstrate it.

The exact opposite is true (5, Informative)

l2718 (514756) | more than 5 years ago | (#25667527)

In fact, Godel proved the exact opposite: that you can make a list of all true statements of mathematics. Godel's completeness theorem states that every statement that follows from the axioms is in fact deducible from the axioms in finitely many logical steps. It is thus possible to enumerate all true statements by enumerating all deductions. Godel also has proved an "incompleteness" theorem. That more famous (and less important) result is that there are statements that are true in specific models yet not provable from the axioms. It implies that there is no algorithm to decide whether a given statement is true -- but this has nothing to do with enumerating all true statements. (Yes, I am a mathematician)

Um, no, no, NO! (5, Informative)

Estanislao Martínez (203477) | more than 5 years ago | (#25667787)

Godel's completeness theorem states that every statement that follows from the axioms is in fact deducible from the axioms in finitely many logical steps.

That Gödel's Completeness Theorem for first-order logic--predicates, individuals, quantifiers ("for all," "exists"), and truth connectives (not, or, and).

Godel also has proved an "incompleteness" theorem. That more famous (and less important) result is that there are statements that are true in specific models yet not provable from the axioms.

The incompleteness theorem is about arithmetic: natural numbers defined in terms of 0 and the successor relation, addition and multiplication. For any set of axioms you pick for arithmetic, there are true statements of arithmetic that cannot be proven from those axioms.

It implies that there is no algorithm to decide whether a given statement is true -- but this has nothing to do with enumerating all true statements.

I'm not completely sure of how relevant the incompleteness of arithmetic is for what you're saying, but I am sure of this: first-order logic is complete, but the validity of a statement in first-order logic is undecidable. Therefore, you don't need to bring in Gödel's incompleteness theorem for arithmetic to conclude that in many important cases.

Re:Um, no, no, NO! (1)

jonaskoelker (922170) | more than 5 years ago | (#25670009)

For any set of axioms you pick for arithmetic, there are true statements of arithmetic that cannot be proven from those axioms.

Or false statements that can be proven. Consider the set of all well-formed formulas.

Re:Um, no, no, NO! (1)

Estanislao Martínez (203477) | more than 5 years ago | (#25671577)

If you picked a set of axioms that could prove a false statement of arithmetic, I wouldn't call those a "set of axioms for arithmetic" in the first place. I know I'm playing a bit fast and loose with all of this, but it does seem clear to me that if a set of axioms proves a statement that isn't true in all models of arithmetic, then one shouldn't be calling it "a set of axioms for arithmetic."

Re:The exact opposite is true (1)

z-j-y (1056250) | more than 5 years ago | (#25668051)

that sounds good, except
1. number theory is not axiomizable, its truth is not effectively enumerable.
2. an axiomized theory is enumberale, but why these axioms? are they consistent? are they ... true?
3. not all theorems are equal, human obviously have a way to focus on "interesting" ones, that's not what a mechanized list can satisfy.
4. enumerability is just theoretical, there is no efficient algorithm at all.

I'm not a mathematician.

Re:The exact opposite is true (1)

bcrowell (177657) | more than 5 years ago | (#25668123)

Godel's completeness theorem states that every statement that follows from the axioms is in fact deducible from the axioms in finitely many logical steps
How would you even define a notion of "follows from the axioms" that didn't presuppose proof in a finite number of steps? If there were a distinction between "provable" and "provable in finite steps," it seems like you'd have to define what it meant to prove something in an infinite number of steps, and then show that for every infinite-length proof there was also a simpler, finite-length one. But I'm really having a hard time imagining what it would mean to have an infinite-length proof of something.

Re:The exact opposite is true (1)

z-j-y (1056250) | more than 5 years ago | (#25668247)

proof implies finite steps. "proof in finite steps" is just to reassure the readers.

Re:The exact opposite is true (4, Informative)

melikamp (631205) | more than 5 years ago | (#25668991)

How would you even define a notion of "follows from the axioms" that didn't presuppose proof in a finite number of steps?

GP is talking about a concept known as logical implication. A set of axioms logically implies a statement if that statement is true in every model satisfying those axioms. A model is a particular interpretation of a set of axioms. Say, if your only axiom is (For all x, For all y (x+y = y+x)) then an abelian group of order two is a model, and so is Z, and so is any mathematical structure where operation + is, in fact, commutative.

"Provable" (or "deducible"), on the other hand, means that there is a finite sequence of formulas which constitutes a formal deduction of a statement from the axioms.

As logicians, we work in the meta-theory, which is widely accepted to be ZFC. A model is just a certain kind of set. Giving a rigorous definition here would be excessive, but we can at least mention that models are "big" objects which include the universe of discourse. So a model for natural numbers omega would, naturally, include the infinite set omega. "A logically implies B" is a statement about how A and B relate in various models. Compare that to "B is deducible from A", a statement about existence of a finite formal deduction, which, in meta-theory, is a different kind of set. A deduction is literally a record of finitely many formulas over a finite alphabet.

Re:The exact opposite is true (1)

melikamp (631205) | more than 5 years ago | (#25668215)

Yes and yes, except that your first sentence is a bit unclear. "That you can make a list of all true statements of mathematics" is just saying that the set is countable.

Re:The exact opposite is true (1)

z-j-y (1056250) | more than 5 years ago | (#25668319)

the set of all statements is countable, so is the subset of all true statements. however, it doesn't mean you can count it:) There "exists" a way to count it, but nobody knows how. (Some people think that's just B.S. and reject such mathematics)

Re:The exact opposite is true (1)

melikamp (631205) | more than 5 years ago | (#25669019)

I agree, I was just saying that the original sentence was somewhat ambiguous, but may be it's just me.

Re:The exact opposite is true (1)

jonaskoelker (922170) | more than 5 years ago | (#25669959)

It is thus possible to enumerate all true statements by enumerating all deductions.

It implies that there is no algorithm to decide whether a given statement is true -- but this has nothing to do with enumerating all true statements.

I'm confused. Please clarify.

If it's possible to enumerate all valid proofs I propose the following proving algorithm: Run through all valid proofs; once you get to a proof whose conclusion is the theorem you want to prove, return that proof.

[if you don't know whether your theorem is true or not, run the above algorithm on its negation as well].

What's wrong with my algorithm?

(Yes, I am a mathematician)

FWIW, At my university, computer scientist are presented with Gödel's theorem before the mathematicians are. Yes, I am a computer scientist. Just in case anyone cares about anyone's credentials more than their arguments.

Re:The exact opposite is true (2, Insightful)

lexDysic (542023) | more than 5 years ago | (#25670313)

If it's possible to enumerate all valid proofs I propose the following proving algorithm: Run through all valid proofs; once you get to a proof whose conclusion is the theorem you want to prove, return that proof.

[if you don't know whether your theorem is true or not, run the above algorithm on its negation as well].

What's wrong with my algorithm?

The problem is that some propositions P have the following two properties:

1: P has no proof
2: (not P) has no proof.

So your algorithm searches forever and you don't know if it just hasn't found anything yet, or if there is nothing to be found.

No, it doesn't work. (2, Insightful)

Estanislao Martínez (203477) | more than 5 years ago | (#25670719)

If it's possible to enumerate all valid proofs I propose the following proving algorithm: Run through all valid proofs; once you get to a proof whose conclusion is the theorem you want to prove, return that proof. [if you don't know whether your theorem is true or not, run the above algorithm on its negation as well].

That needs a couple of small amendments:

  1. You shouldn't run the algorithm on the statement and its negation in sequence, because the basic algorithm will never terminate for an unprovable statement. To harden the algorithm, you should interleave the runs for the statement and its negation: as you enumerate each valid proof, you check whether the conclusion is either your statement or its negation.
  2. Strictly speaking, what's relevant here is not the "truth" of a statement, but rather its validity given the axiomatic theory. A valid statement is one that is true under all interpretations of the theory; an invalid statement is false under all interpretations of the theory; a contingent statement is one that's neither valid nor invalid, since it's true under some interpretations of the theory and false under others.

Intuitively, your algorithm fails if the theory admits of contingent statements (as first-order logic does), or if the theory is incomplete (as arithmetic is). If you feed it a contingent statement, it will never terminate, since no proof will have either the statement or its negation as its conclusion. Same goes if your theory is incomplete and you feed it one of its Gödel sentences.

If you can prove that for every statement in the language, your axiomatic theory has a proof either of that statement or its negation, then your algorithm works for that theory. (The textbook I used calls such theories syntactically complete, but books often use just "complete" for this property, which is different from Gödel's "(in)completeness"...)

(All of the above assumes the axiomatic theory is sound to start with, i.e., there are no proofs of invalid statements. If your theory is unsound, you've got bigger problems.)

Re:The exact opposite is true (1)

Zalbik (308903) | more than 5 years ago | (#25671073)

In fact, Godel proved the exact opposite: that you can make a list of all true statements of mathematics

You must be using some obscure meaning of "true" I am not aware of.

Godel proved that the set of true statements is uncountable. There is no countable set of axioms that can be added to number theory that make it complete. If the truths of mathematics were countable, this would not be so.

As Wikipedia put's it:
"Gödel's theorem shows that, in theories that include a small portion of number theory, a complete and consistent finite list of axioms can never be created, or even an infinite list that can be enumerated by a computer program. " here [wikipedia.org]

IIRC, the set of provable statements in mathematics is countable...

Re:The exact opposite is true (1)

mapkinase (958129) | more than 5 years ago | (#25671199)

Godel's result is rather philosophical, than technological (and not scientific, of course). It gives you idea that the most fine technology that humans come up with - math - is short-ranged, finite, which logic breaks at far range. And that is fine for real life apps.

It limits logic, which is a sign for us not to put it on top. It is a mathematical equivalent of finiteness of human experience.

There are things beyond of our scope. Some of them are not important, and some of them are and we cannot handle them scientifically.

Greatest minds that came to the frontier of the science of their time realized that.

Re:what is a central theorem? (5, Informative)

sustik (90111) | more than 5 years ago | (#25668773)

> Godel of course proved that you can never have a complete list of all true statements in mathematics.

Bzzzt. Wrong.

What Godel proved was that all mathematical thruths cannot be described by a finite axiom system. The statement that there is a single empty set cannot be proved. Similarly continuum = aleph_1 cannot be proved; in both cases one may argue that these are so "obvious" that they need to be accepted as axioms.

Note that continuum = aleph_1 was a strongly accepted conjecture as much as the Riemann hyp today.

I studied set theory and models. It is fascinating that you can have a countable model of set theory! This model is basically built from a countable set with countable many subsets accepted as sets, etc. The rest of the subsets an "outsider" can see are not known inside the model. We denote this model (which is a counatble set for the ousider aka meta theory) by M. The natural numbers are in M, denote it by A. A is known in the model and A is an infinite (countable) set.

The set containing the subsets of A, denoted by P(A) is different depending on whether you look inside or outside the model! Outside it is an uncountable set, of course. In the model world it is Pm(A) and it appears uncountable again, but for the outside observer it is actually the intersection of P(A) and M. Bear with me another minute!

In the model world of M the Pm(A) appears not countable. What does that mean? It means that there is no 1-1 mapping between A and Pm(A). In the outside there is a mapping of course, since both sets are countably infinite. This mapping (a function) is actually a set (everything is a set: function, relation etc.) so a mapping denoted by F between A and Pm(A) exists outside. However F is not an an element in M so it does not exist inside the model.

There is a way to extend the model M into something called M(F) by 'forcing' F to be in M. Basically we add F and everything else that need to be added to still have a valid theory inside M. It is not trivial to do this, it was discovered and proved by P. Cohen an analysis guy (not a set theorist). Set theorists of course run with this ever since. The careful picking of F allows different M(F)-s to be created and that leads to results showing that continuum = aleph_1 is not the only possibility. One can 'force' a bunch of other alephs under the continuum. (What aleph exactly can continuum be is also interesting to set theorists at least.)

Now there is one model called L which consists of the 'constructible' sets and nothing else. In L continuum=aleph_1. There are in fact theorems based on the assumption that V = L, that is V the world consists of only constructible sets.

You may wonder how this L can be defined. I cannot go into the details, but one eye-opening fact though is that you can define Lm inside the above M model!!! This Lm is a countable model of L and in some sense a minimal model of set theory if I recall correctly.

So one may take the position that we want mathematical thruths in L the minimal system. (This resonates with Occam's razor.) Of course note that there is no axiomatic system describing L.

I want to emphasize that if we fix a model then each statement has a truth value; but there exist truths which cannot be proved working inside the model only.

For the usual applied math we could say we assume V=L. (Or any other well defined model for that matter.) Note againg that aleph_1 == continuum in L, because there are no other alephs that could fit "between". The mathematicians inside L see this as this: we cannot prove that aleph_1 == continuum in fact there could be something between, but it is not constructible from what we have.

I hope this helped.

Tagged Supercomputing (2, Interesting)

lazynomer (1375283) | more than 5 years ago | (#25667309)

Do you really need supercomputers in all practical cases?

Re:Tagged Supercomputing (4, Informative)

fractic (1178341) | more than 5 years ago | (#25667509)

No, in general formalizing a proof does not require a lot of computer power. Usually it takes a lot of man power instead. Most current proof assitants are actually proof verifiers. The user has to break down the proof to elementary steps that the program can verify.

Now sometimes a computer is used to verify a lot of cases by brute force computation. Often this is not done in an actual proof assistant but within a computer algebra package. But this is also met with a sceptical eye.

The four colour theorem is perhaps one of the most famous formalized theorems. It was orginally proven by a large computation. But noone could really verify this. Recentely (2004) it was formalized completely in the proof assistant Coq (actually a custom extension). This formalized proof did require a lot of computer time allthough just on a normal computer, not a supercomputer.

Re:Tagged Supercomputing (1)

lazynomer (1375283) | more than 5 years ago | (#25667733)

I suspected as much; thanks for your answer.

Still, ain't it super computers can help mathematicians?

Which central theorems (1)

florescent_beige (608235) | more than 5 years ago | (#25667361)

aren't already proven? Principia Mathematica did the basics and I always assumed more advanced theorems became proven as required.

Maybe someone just wants to do Principia Mathematica volumes II through L but doesn't that already in effect exist?

Re:Which central theorems (3, Informative)

bcrowell (177657) | more than 5 years ago | (#25668427)

Which central theorems aren't already proven? Principia Mathematica did the basics and I always assumed more advanced theorems became proven as required. Maybe someone just wants to do Principia Mathematica volumes II through L but doesn't that already in effect exist?

Well, one issue is that the Principia Mathematica undoubtedly has errors in it. No human being could ever write a book of that length without making a single mistake. So there could be some value in producing the same results on a computer, which doesn't make the same kind of mistakes a human does. Another issue is that the Principia Mathematica works within a certain axiomatic framework, and I believe that framework is different from the most popular axiomatic framework used today, which is Zermelo-Fraenkel set theory, with the axiom of choice (ZFC). (They were both produced around 1910, but the WP article says that PM used a complicated system of types, which is probably different from anything in ZFC.)

More broadly, for people who are interested in the foundations of mathematics, there's no clear way to decide that one set of axioms is superior to another. Some people feel that ZFC is too strong, because it asserts the existence of things that can't be explicitly constructed. Those people may be interested in seeing how much of mathematics can be proved using purely constructive methods. With a weaker set of axioms, some results may be impossible to prove, while others may be possible to prove, but the proofs may be extremely long compared to the proofs in ZFC -- so long that using a computer may be a real help.

Still other people are interested in seeing what can be done in an axiomatic system that's stronger than ZFC. For instance, such a system may have sizes of infinities that are larger than the sizes of the infinities in ZFC, and they may even have creatures like the set of all sets. One thing that tends to happen when you try to make stronger axiomatic systems is that it becomes much more difficult to avoid internal inconsistencies. I can imagine that a computer could be helpful in finding things like that. If you're fiddling around with the computer proof system and it comes up with a result that 1+1=3, then you've learned something interesting: your set of axioms is bogus.

One thing you really have to be careful about if you're working in this kind of field is that you don't want to inadvertently assume some result that someone else has proved in some other axiomatic system, and that seems obvious to you, but that actually isn't provable (or hasn't yet been formally proved) in the system you're working in. That's the kind of thing where I'd imagine a computer system would be really helpful. It wouldn't allow you to make those assumptions. In general, if you look at almost all published mathematical work, it never states which axiomatic system it's assuming, and that's because in most fields of mathematics we expect that the results are unlikely to depend on which particular foundation you're working in. E.g., I doubt that Wiles' proof Fermat's last theorem even bothers to state that it starts from ZFC, and most mathematicians probably have a strong expectation that it doesn't matter whether you pick some other foundation, Wiles' proof will still be valid. Nevetheless, it's possible that that's not true. Abraham Robinson, for example, claimed that ZFC had been carefully engineered to make the real number system work correctly, and therefore claimed if you wanted to use a different system of numbers (such as the hyperreals, a system that includes Newton- and Leibniz-style infinities), you might be better off using diffrent axioms.

Re:Which central theorems (1)

z-j-y (1056250) | more than 5 years ago | (#25668585)

and most mathematicians probably have a strong expectation that it doesn't matter whether you pick some other foundation, Wiles' proof will still be valid.

what do you mean by a proof being valid in another set of axioms? that there is a simple way to translate the proof into the 2nd system and it'll be true then?

Re:Which central theorems (1)

bcrowell (177657) | more than 5 years ago | (#25668693)

what do you mean by a proof being valid in another set of axioms? that there is a simple way to translate the proof into the 2nd system and it'll be true then?
yes

Re:Which central theorems (1)

DiegoBravo (324012) | more than 5 years ago | (#25668877)

>> So there could be some value in producing the same results on a computer, which doesn't make the same kind of mistakes a human does.

Except if it has one of the first Pentium's...

Seriously, even if the "math prover" is right, who proves the "math prover"?

Re:Which central theorems (1)

John Hasler (414242) | more than 5 years ago | (#25670997)

> Except if it has one of the first Pentium's...

Which doesn't make the same kind of mistakes humans do.

> Seriously, even if the "math prover" is right, who proves the "math prover"?

The point is that if a human and a computer agree it is more likely that they are right than when two humans (or two computers) agree because the weaknesses of the human and the computer differ.

Uh... (0)

Anonymous Coward | more than 5 years ago | (#25667433)

One long-term dream is to have formal proofs of all of the central theorems in mathematics

And what theorems would *those* proofs be based on?

Re:Uh... (1, Informative)

florescent_beige (608235) | more than 5 years ago | (#25667459)

Axioms.

Re:Uh... (0)

Anonymous Coward | more than 5 years ago | (#25668183)

Axioms.

boy.do.i.feel.dumb.

Answer me this... (0)

Anonymous Coward | more than 5 years ago | (#25667549)

Benchmarks have shown that Via processors have much lower floating-point performance compared to their competitors (i.e. Intel and AMD) so why exactly are they using Via chips to achieve mathematical proofs?

Re:Answer me this... (1)

fuzzyfuzzyfungus (1223518) | more than 5 years ago | (#25667713)

You do realise that there is more to math than arithmetic, right? There are very large areas of mathematics that can be done with very minimal computation, float or int, and a fair few areas that don't need numbers at all. Many, though not all, proofs fall in this category.

Proof is discrete (4, Insightful)

Estanislao Martínez (203477) | more than 5 years ago | (#25667919)

Benchmarks have shown that Via processors have much lower floating-point performance compared to their competitors (i.e. Intel and AMD) so why exactly are they using Via chips to achieve mathematical proofs?

A formal proof is not a numerical calculation. A formal proof is, basically, a set of premises, a conclusion, and a set of steps that justifies the conclusion, given those premises and a set of rules that define your proof system. The premises and conclusions are logical formulas, which are basically symbolic trees, and the proof steps relating the premises to the conclusion are all discrete too. So there is no essential numerical calculation going on at any point here.

Re:Answer me this... (2, Insightful)

colmore (56499) | more than 5 years ago | (#25668127)

Knowing a little bit about formal proofs and a fair bit about programming, but nothing about the computerized verification or generation of formal proofs, I really doubt the FPU is used for this stuff.

math doesnt matter (-1, Flamebait)

Anonymous Coward | more than 5 years ago | (#25667771)

what matters is that we finally have a black president. that's all we need. our lives are saved.

Re:math doesnt matter (1)

boshi (612264) | more than 5 years ago | (#25667835)

But can you prove it computationally?

Re:math doesnt matter (1)

colmore (56499) | more than 5 years ago | (#25668141)

Unfortunately his presidency will either be incomplete or inconsistent.

And then there are leaders out there like Castro, who doesn't seem to halt.

Metamath Proof Explorer (4, Informative)

Manchot (847225) | more than 5 years ago | (#25667783)

There's a website called Metamath [metamath.org] which does a lot of what the article is talking about. It starts from the ZFC axioms and works its way up to thousands of elementary theorems, all proved completely formally. Pretty cool, if you're in to that sort of thing.

Important for the long term evolution of CAS (4, Interesting)

starseeker (141897) | more than 5 years ago | (#25668227)

CAS, or Computer Algebra Systems, represent one of the most useful tools for handling practical application of complex mathematics. The package Feyncalc, built on Mathematica and used for High Energy Physics, is one such example. The problem with using these systems is that they can't be trusted by the people using them. There is always that risk of "did the programmer do something that buggered this case" or "did they get that formula wrong when they translated it to code?" The traditional answer is a combination of by-hand verification and learning to "trust" certain abilities of some systems over time - lots and lots of use creates a certain confidence that the bugs have been shaken out of well-used functionality. But that lingering doubt remains - "is it REALLY right?"

There are philosophical questions at the root of this issue. On the most abstract level is the question of whether knowing something is true is important compared to knowing WHY it is true - purists might argue if we don't know the latter the problem isn't answered. I'll state up front that for the problem I'm interested in solving - KNOWING my answer to a problem is correct - I'm willing to trust a machine that is proven by humans to be able to verify proofs as correct to verify MY solution to a particular problem. Or, put another way, that once the correctness of the checker is proven all statements of correctness from that checker are also proven. This is not a universal assumption, but if one is willing to make it things get interesting.

Most proofs mathematicians attempt are not the types of problems posed by high energy physics - proving the solution to a specific integral is the correct solution would be of minimal value as a mathematical revelation. For the practical focus of scientific use of CAS however, the question of whether the system just gave the correct solution to that integral is all important. Moreover, the mathematical axioms behind the statement of correctness are not of immediate concern - they interest mathematicians, but the physicists want to USE that result. There's a contradiction here, because to be trustworthy in a mathematical sense the foundational system within which that integral was evaluated and what assumptions were made in the process MUST be considered. What to do?

Trustworthy computer verification of proofs offers an answer to this dilemma. A CAS designed to incorporate proof logic awareness into its core system and algorithms could be asked to produce a "proof" of its answer based on the steps it used to create that answer. This proof can then be subjected, just like any human written proof, to the rigors of verification. A human COULD (in theory) do the checking if they wanted to. In practice, an incorporated proof verifier could examine the CAS's proof for flaws. If none were found, for the specific problem in question, the user could then know that the answer they have IS correct, regardless of any potential flaws in the CAS (which will hopefully be reduced dramatically by the design rigors needed to implement routines that can support supplying the proof logic in the first place). The trust tree has been reduced to the proof verification routine and the software and hardware needed to run it, which is a MUCH smaller trust tree than the whole of the CAS.

The practical realization of such a system is probably decades in the future. It could be done only as an open source system, where the entire mathematical and scientific community contributed to an ever expanding body of trusted knowledge which could be built upon. Many extremely difficult problems would need to be solved - an immediate problem is how to organize mathematics into a coherent framework in a scalable way via computer. Category theory is probably the answer, but what does that mean in terms of system implementation? What about the programming language that must be put behind the mathematical definitions, even if the conceptual framework of Category Theory in Computer is addressed? What are the techniques needed for trustable proof verification, and how will the necessary human verification of the core trustworthy systems be documented? etc etc etc...

It's a fascinating problem, one I hope to see much more work on as the years go by. Despite the difficulties, I think such systems will be necessary for continued research, because the human mind's ability to gain and use knowledge is limited by our I/O capacity and the inevitable consequences of age. There will come a time when we desire to solve problems that cannot fit within the constraints of the human brain as it is currently housed, and when that time comes we MUST have machines that we can trust.

Re:Important for the long term evolution of CAS (1)

Creepy Crawler (680178) | more than 5 years ago | (#25668481)

Hence why programs proving theorems should be proved also.

Also the program should catch OS inconsistencies an direly alert them to the user of the CAS, as those could create errors also.

Inevitable Godel's Theorem discussion (0)

Anonymous Coward | more than 5 years ago | (#25669103)

Godel's Theorem has to be the most misunderstood statement of all time. I won't attempt a statement here because, right or wrong, I will get 10 incorrect corrections, maybe one correct one. There's kind of a mini Godwin's law in effect for any discussion here about something with the words "automated" and "theorem" in the title. Inevitably it will devolve into bickering about Godel's Theorem, even though it *plays no role at all in what these projects are trying to accomplish*. They merely want to record a giant database of theorems and proofs, to aid in finding further theorems and proofs. Even without Godel's Theorem, since there are infinitely provable statements, the list would never be complete anyways.

BS (1)

Secret Rabbit (914973) | more than 5 years ago | (#25670015)

It is nothing but BS that the computer is better than human. Not to mention profound stupidity to think that the computer is infallible i.e. it is programmed by humans.

I read the first bit of Freek Wiedijk's article and it's political nonsense. All they've done is use the word "formalization" to describe the process of encoding mathematics "in the computer". What this does is hijack the common notion of formalization for use for there own purposes. Because, formalization is good, right? Well, not if you read and really understand what it does, and infinitely more important, does NOT mean in this context.

Point of fact, using computers does NOT take human minds out of the equation. It just hides them giving people the illusion of a more effective system.

Load More Comments
Slashdot Login

Need an Account?

Forgot your password?