Computer-verified Mathematical Proof as Standard
Andrew Tomazos
series of well-defined logical deductions from some set of axioms and
rules?
If yes, is it also true that all of these deductions could be written
in such a way that a computer program can infallibly verify the
correctness of these steps?
If also yes, than why isn't it required that the centerpiece of any
published proof be the "source code" for such a computer verification?
ie Shouldn't the center of every proof be a machine-readable theorem
and machine-readable steps to undeniably deduce that theorem? The
English should just be annotation essentially.
Furthermore, why isn't there a centralized proof web/database that
contains all the axioms and verified proofs in some standard format?
If we had some standard naming reservation system than you could use
an old theorem from one verified proof in the database as a "basis
axiom" for a new proof.
What am I missing?
-Andrew.
Spiros Bousbouras
> Is it true that all proofs of mathematical theorems must contain a
> series of well-defined logical deductions from some set of axioms and
> rules?
The general idea is that every proof can be written in the way you
specify. But for actual published proofs this hardly ever
happens. A lot , probably most mathematicians don't even know what
a formal derivation is. They rely on experience and intuition to
decide that the steps in their proofs are valid. Even those who do
know what a formal derivation is more often than not rely on
intuition to decide that their proofs could be expanded to formal
derivations because actually writing them this way would be too
much work and due to its tedious nature may actually increase
mistakes rather than reduce them.
> If yes, is it also true that all of these deductions could be written
> in such a way that a computer program can infallibly verify the
> correctness of these steps?
If the verifier does not contain bugs and runs on top of an
operating system whose possible bugs will not adversely influence
the correct functioning of the verifier and both the verifier and
the operating system run on top of hardware whose possible bugs
will not adversely influence the correct functioning of the
verifier and the verifier receives correct input then the answer is
yes. There are several programmes which do this.
> If also yes, than why isn't it required that the centerpiece of any
> published proof be the "source code" for such a computer verification?
Because mathematics proofs have existed for a lot longer than
computers and there isn't a strong enough incentive to change
things.
> ie Shouldn't the center of every proof be a machine-readable theorem
> and machine-readable steps to undeniably deduce that theorem? The
> English should just be annotation essentially.
Why do you think it should ? It's not obvious that it will increase
correctness. Note that many computer programmes have silly bugs
which a human reader would immediately pick up but a compiler might
not. So it is possible that due to such a silly bug in the source
of a proof the computer will say that a proof is correct when
actually it is not.
> Furthermore, why isn't there a centralized proof web/database that
> contains all the axioms and verified proofs in some standard format?
http://en.wikipedia.org/wiki/Mizar_system
> If we had some standard naming reservation system than you could use
> an old theorem from one verified proof in the database as a "basis
> axiom" for a new proof.
>
> What am I missing?
One of the things I want to try out at some point is to write my
own proof verifier and see how it affects my productivity and
whether using it to verify proofs might introduce mistakes I wouldn't
otherwise make. So basically I believe more experimentation is
needed by as many mathematicians as possible before reaching
conclusions.
--
Who's your mama?
Musatov
Dear Andrew,
You raise an essential question of time and information gathering.
If resources are not centralized to be accesible they are not
exercised to full extent, but when they are leveraged from a central
form or resource what limits can be upon them?
The answer is a time/possibility governed equation. Godel embraced
impossibility but failed to see he could not possibly understand all
the ways and possibilities a truthful condition is reached.
I can only see ignorance in this base philosophy, but then again
perhaps it is me who is ignorant, as I will not entirely rule out the
impossibility only specifically to this man, Godel.
The inverse possibility of a completeness theorem is properly governed
by the number of ways a condition is reached.
We may say with great certainty a child was born today, for example.
If we do not have the circumstances of the families of every single
family a child was born today, the certainty of one child being born
today is certain.
This is to say, although we may perceive with certainty, we attempt to
compile a list of circumstances, to the best of our ability.
However, the big delinieation here is the fact there is no correlation
between us being able to compile a complete list of characteristics,
and a complete set of these characteristics existing.
We can in fact state with great certainty every child born today came
from a family with circumstances. Our ability to make a complete list
has absolutely no bearing on this existence and it in fact also does
not keep us from compiling a real usable list of circumstances of
families wherein a child was born today.
Further if this list is prepared it does not cease to be useless
because of the level of completeness in it.
Godel is a paradox of reason. We can state with certainty there is a
number of ways and possibility a certainty is reached. The number of
ways and possibility has no bearing on the certainty of whether the
condition is perceived. The perception of this certainty bears no
impact on the usability of partial pieces of information.
P = NP problem - Wikipedia, the free encyclopedia
The information needed to verify a positive answer is also called a
certificate. <....> Other solutions violate the Turing machine model
on which P and NP are <...>
http://en.wikipedia.org/wiki/P_%3D_NP_problem
BletchleyPark.net - Time Complexity - P and NP Classes
In general, researchers believe that P NP, because ever since 1971,
extensive and <...> where as class NP problems have solutions that can
be verified quickly. <...> A nondeterministic machine allows for more
than one outgoing transition <...>
http://www.bletchleypark.net/algorithms/Time_Complexity_P_vs_NP.html
[PPT] The P=NP problem
IF P = NP then problems like the subset-sum problem are as "easy" to
compute as to verify. <...> machine M that takes the solution to be
verified as input. <...>
http://www.math.nmsu.edu/~jlakey/m210/Lecture6_fa08.ppt
Wapedia - Wiki: P = NP problem
The relationship between the complexity classes P and NP is an
unsolved <...> to our problem can be verified in polynomial time, so
this problem is in NP. <...> deterministic sequential machine in an
amount of time that is polynomial in the <...>
http://wapedia.mobi/en/P_%3D_NP_problem
Complexity Classes P And NP Problem Time Problems Polynomial
In essence, the P = NP question asks: if positive solutions to a YES/
NO problem can be verified quickly, can the answers also be computed
quickly? <...> If there is an algorithm (say a Turing machine, or a
LISP or Pascal program with <...>
http://www.economicexpert.com/a/Complexity:classes:P:and:NP.htm
What's "P=NP?", and why is it such a famous question? - Stack Overflow
I really don't see how you explain P and NP without Turing machines.
<...> However, it is harder to see why something verified in P-time
may ever be computed <...>
http://stackoverflow.com/<...>/whats-pnp-and-why-is-it-such-a-famous-question
P = N...@Everything2.com
However, it would appear absurd that P=NP. A nondeterministic machine
trying to <...> can be verified in polynomial time by a deterministic
Turing machine. <...>
http://everything2.com/title/P%2520%253D%2520NP
[PDF] Approaching P=NP: Can Soap Bubbles Solve The Steiner Tree
Problem <...>
Jun 14, 2006 <...> time and NP contains problems whose answers can be
verified in <...> machines, and so can perform computation, and hence
fall under P, <...>
http://www.tjhsst.edu/~rlatimer/techlab06/Students/OuyangPaper06F.pdf
NP-complete - Wikipedia, the free encyclopedia Jun 21, 2008 <...>
Any given solution to the problem can be verified quickly (in
polynomial <...> A problem p in NP is also in NPC if and only if every
other problem <...> machine) for C, we could solve all problems in NP
in polynomial time. <...>
http://en.wikipedia.org/wiki/NP-complete
Complexity classes P and NP. Who is Complexity classes P and NP <...>
Definition of Complexity classes P and NP in an online ecyclopedia or
dictionary. <...>
a deterministic sequential machine in an amount of time that is
polynomial in the <...>
can be verified in polynomial time given the right information, <...>
http://knowledgerush.com/kr/encyclopedia/Complexity_classes_P_and_NP/
P=NP.
Q.E.D.
M.M.M.
[Mathematics is logic and numbers. Inverse 19]
Spiros Bousbouras
> in such a way that a computer program can infallibly verify the
> correctness of these steps?
>
> If also yes, than why isn't it required that the centerpiece of any
> published proof be the "source code" for such a computer verification?
Related to your question is
< http://en.wikipedia.org/wiki/Kepler_Conjecture#A_formal_proof >
H. J. Sander Bruggink
> Is it true that all proofs of mathematical theorems must contain a
> series of well-defined logical deductions from some set of axioms and
> rules?
Yes and no. What you mention above is a formal proof. The proofs you'll
find in paper are (usually) not formal proofs. Rather, they are
arguments that convince mathematical peers that a formal proof for the
theorem exists.
>
> If yes, is it also true that all of these deductions could be written
> in such a way that a computer program can infallibly verify the
> correctness of these steps?
Yes. Formal proofs can be verified easily.
>
> If also yes, than why isn't it required that the centerpiece of any
> published proof be the "source code" for such a computer verification?
>
> ie Shouldn't the center of every proof be a machine-readable theorem
> and machine-readable steps to undeniably deduce that theorem? The
> English should just be annotation essentially.
That would eliminate human error, yes. However, requiring that all
proofs be machine-checkable would probably slow down mathematical
research, because creating a formal, machine-checkable proof typically
takes much longer. Also, humans read natural language much easier than a
formal language, so proofs in English are much easier to read and
understand. Most mathematicians prefer understanding a proof themselves
over a computer saying that the proof is correct.
Having said that, there are research groups working on translating known
mathematical proofs to a machine-checkable format. Maybe
http://www.cs.ru.nl/~herman/FormMath.html would interest you.
>
> Furthermore, why isn't there a centralized proof web/database that
> contains all the axioms and verified proofs in some standard format?
> If we had some standard naming reservation system than you could use
> an old theorem from one verified proof in the database as a "basis
> axiom" for a new proof.
Well, first of all, there is no standard format. For exactly the same
reason that there is no standard programming language: mathematicians
have different requirements, tastes, etc.
groente
-- Sander
William Elliot
> Is it true that all proofs of mathematical theorems must contain a
> series of well-defined logical deductions from some set of axioms and
> rules?
>
Yes.
> If yes, is it also true that all of these deductions could be written
> in such a way that a computer program can infallibly verify the
> correctness of these steps?
>
No.
> If also yes, than why isn't it required that the centerpiece of any
> published proof be the "source code" for such a computer verification?
>
Because it would be necessary to prove that the code had no errors.
> ie Shouldn't the center of every proof be a machine-readable theorem
> and machine-readable steps to undeniably deduce that theorem? The
> English should just be annotation essentially.
No.
> Furthermore, why isn't there a centralized proof web/database that
> contains all the axioms and verified proofs in some standard format?
The closest you'll ever get to that is university math libraries.
> If we had some standard naming reservation system than you could use
> an old theorem from one verified proof in the database as a "basis
> axiom" for a new proof.
Principia Mathematica, by Burtran Russel was a large three volume
work that did no more than prove the very basics of logic and set theory.
Upon publication, besides the usually errata, it was found to have fatal
flaws.
> What am I missing?
Lack of naivete.
Do you know about Mizar?
Spiros Bousbouras
>
> Principia Mathematica, by Burtran Russel
That's Bertrand Russell.
Andrew Tomazos
> > If yes, is it also true that all of these deductions could be written
> > in such a way that a computer program can infallibly verify the
> > correctness of these steps?
>
> If the verifier does not contain bugs and runs on top of an
> operating system whose possible bugs will not adversely influence
> the correct functioning of the verifier and both the verifier and
> the operating system run on top of hardware whose possible bugs
> will not adversely influence the correct functioning of the
> verifier and the verifier receives correct input then the answer is
> yes. There are several programmes which do this.
Yes, but couldn't the language that the machine-readable proof is
written in be specified as a standard. That way several
implementations of verifiers could be developed for different hardware
and operating systems (as is common for most heavily used programming
languages).
It seems as though the basic rules of verifying FOL from an
implementation point-of-view are quite trivial. ie There isn't a lot
that could go wrong. In any case, surely we must agree that such a
system would be significantly more reliable than what we do now.
> > If also yes, than why isn't it required that the centerpiece of any
> > published proof be the "source code" for such a computer verification?
>
> Because mathematics proofs have existed for a lot longer than
> computers and there isn't a strong enough incentive to change
> things.
Well, the incentive is that we would have a near infallible and
scientific way to verify any mathematical theorem - with an instant
and impartial peer-review process. Surely it would save a lot of time
in determining whether a proof is valid or not.
> > ie Shouldn't the center of every proof be a machine-readable theorem
> > and machine-readable steps to undeniably deduce that theorem? The
> > English should just be annotation essentially.
>
> Why do you think it should ? It's not obvious that it will increase
> correctness. Note that many computer programmes have silly bugs
> which a human reader would immediately pick up but a compiler might
> not. So it is possible that due to such a silly bug in the source
> of a proof the computer will say that a proof is correct when
> actually it is not.
I don't see how it could not increase correctness? How could a machine-
verified proof be incorrect? What is an example of a "silly bug" that
might be in a theorem verifier? It seems like all the steps to verify
a proof are very straightforward and simple. The steps seem ideally
suited to machine.
> > Furthermore, why isn't there a centralized proof web/database that
> > contains all the axioms and verified proofs in some standard format?
>
> http://en.wikipedia.org/wiki/Mizar_system
Very interesting. This "Mizar system" and the "QED project" are
exactly what I am suggesting. My question is why haven't they evolved
into the standard way of publishing proofs?
> > If we had some standard naming reservation system than you could use
> > an old theorem from one verified proof in the database as a "basis
> > axiom" for a new proof.
>
> > What am I missing?
>
> One of the things I want to try out at some point is to write my
> own proof verifier and see how it affects my productivity and
> whether using it to verify proofs might introduce mistakes I wouldn't
> otherwise make. So basically I believe more experimentation is
> needed by as many mathematicians as possible before reaching
> conclusions.
I'm sure writing a machine-readable proof is more difficult than
taking some steps for granted or based on intuition - but the
advantage of the former is that it is virtually infallible. Isn't
that what mathematics is all about? Rigorous and undeniable steps
from axioms to theorems?
-Andrew.
Andrew Tomazos
Yes, but this is a proof by exhaustion. I'm asking why all kinds of
proofs are not required to be machine verified?
-Andrew.
Andrew Tomazos
> > If also yes, than why isn't it required that the centerpiece of any
> > published proof be the "source code" for such a computer verification?
>
> Because it would be necessary to prove that the code had no errors.
This is a completely illogical position. A proof must be published in
some language. Currently most are published in a mix of natural
language and mathematical notation. Is it necessary to prove that the
humans that read and approve these proofs contain no errors before
making them theorems? Of course not.
What I am suggesting is that we specify a standard language that all
mathematical proofs are written in, that both humans and computers can
read and verify. It seems this is exactly what Mizar is. It seems as
though if we did this it would be far quicker and more rigorous than
what we do now. It also seems like the basic rules of transformation
from one statement to another are so simple, that any bugs contained
in verifier implementations would quickly and easily be eradicated.
> Principia Mathematica, by Burtran Russel was a large three volume
> work that did no more than prove the very basics of logic and set theory.
> Upon publication, besides the usually errata, it was found to have fatal
> flaws.
Exactly my point. If "Principia Mathematica" was written in machine-
readable format, than the verifier software would of caught these
errors wouldn't it?
-Andrew.
Andrew Tomazos
wrote:
> Andrew Tomazos wrote:
> > Is it true that all proofs of mathematical theorems must contain a
> > series of well-defined logical deductions from some set of axioms and
> > rules?
>
> Yes and no. What you mention above is a formal proof. The proofs you'll
> find in paper are (usually) not formal proofs. Rather, they are
> arguments that convince mathematical peers that a formal proof for the
> theorem exists.
Interesting. So we call something a theorem even if no formal proof
has been written. Perhaps we need another level above theorem like
'formal fact' to define a statement that has a written formal proof.
> > ie Shouldn't the center of every proof be a machine-readable theorem
> > and machine-readable steps to undeniably deduce that theorem? The
> > English should just be annotation essentially.
>
> That would eliminate human error, yes. However, requiring that all
> proofs be machine-checkable would probably slow down mathematical
> research, because creating a formal, machine-checkable proof typically
> takes much longer.
Well given that real mathematical facts are true for all time - it
would seem sensible to take the effort to write out the formal proof.
It only has to be done once right? - and then it is done for time
immortal.
> Also, humans read natural language much easier than a
> formal language, so proofs in English are much easier to read and
> understand. Most mathematicians prefer understanding a proof themselves
> over a computer saying that the proof is correct.
Interesting. As a computer scientist we think a lot about what makes
language both machine-readable and human-readable. One of the design
goals of XML for example was to do both. It might be possible to come
up with a language for formal proofs that achieves both goals.
I imagine that many proofs in natural language are hard to read due to
ambiguities. We have all heard of the term "write only journal". Is
it possible that there exists a machine-readable formal language that
may actually *increase* comprehension by humans?
> Well, first of all, there is no standard format. For exactly the same
> reason that there is no standard programming language: mathematicians
> have different requirements, tastes, etc.
Yeah, I thought a bit about this. If we consider the basic rules of
predicate calculus and FOL as a type of primitive "machine code", and
we provide a way to define a new notation in terms of that machine
code - it would be possible to write "notation modules".
"Notation modules" and "formal proofs" could be universally identified
in a similar way that we do with domain names on the Internet. Once
named they could be authenticated and uploaded into a distributed
database.
Each individual mathematician could choose which modules they want to
use or write there own. Groups of mathematicians could share these
notation modules and import them into their proofs by referencing
their universal name. Eventually some notation modules could become
so heavily used that they become defacto standards. We have seen this
happen in similiar systems.
In any case, it would be possible to create a domain-specific notation
- but the compiled version would result in the same easily verifiable
primitive statements in terms of predicate logic and FOL.
This would address the concern of mathematicians have different
requirements and tastes for how they express their formal proofs.
-Andrew.
Andrew Tomazos
> One should not confuse computer science with mathematics
> for they are two distinctly different things -- Bertrand Russell
Using computers to verify mathematical proofs no more confuses
computer science with mathematics, than using telescopes to view stars
confuses optics with astronomy -- Andrew Tomazos
G. A. Edgar
> Furthermore, why isn't there a centralized proof web/database that
> contains all the axioms and verified proofs in some standard format?
> If we had some standard naming reservation system than you could use
> an old theorem from one verified proof in the database as a "basis
> axiom" for a new proof.
>
Perhaps the proper question is: when will such verified proofs and
standard format become the norm? 10 years from now? More? Less?
> See
>
> http://www.ams.org/notices/200811/index.html
A question is which of the present systems will become the standard, or
maybe a new not-yet well-known system will be adopted instead.
If the OP really wants to know why it is not done routinely now, he
should take a favorite theorem and put it into one of these systems.
Then report back on his experiences.
> Principia Mathematica, by Burtran[d] Russel was a large three volume
> work that did no more than prove the very basics of logic and set theory.
>
> Upon publication, besides the usually errata, it was found to have fatal
> flaws.
incorrect
--
G. A. Edgar http://www.math.ohio-state.edu/~edgar/
Frederick Williams
> > Principia Mathematica, by Burtran[d] Russel was a large three volume
> > work that did no more than prove the very basics of logic and set theory.
> >
> > Upon publication, besides the usually errata, it was found to have fatal
> > flaws.
>
> incorrect
Three times over: both paragraphs are wrong and Bertrand Russell spelled
his name as I have just done.
--
Narouz began to feel the tuggings of the Underworld, the five wild dogs
of the sense pulling ever more heavily upon the leash. He opposed to
them the forces of his mighty will, playing for time, waiting for the
only human revelation he could expect--voice and odour of a girl who
had become embalmed by his senses, entombed like some precious image.
H. J. Sander Bruggink
> On Jun 19, 11:38 am, "H. J. Sander Bruggink" <brugg...@uni-due.de>
> wrote:
>> Yes and no. What you mention above is a formal proof. The proofs you'll
>> find in paper are (usually) not formal proofs. Rather, they are
>> arguments that convince mathematical peers that a formal proof for the
>> theorem exists.
>
> Interesting. So we call something a theorem even if no formal proof
> has been written. Perhaps we need another level above theorem like
> 'formal fact' to define a statement that has a written formal proof.
I meant to say that proofs in journals typically are not written in a
formal language. So yes, that means that there are theorems for which no
formal proofs have been written. However, the proofs in journal articles
are typically, although written in a natural language, very precise, so
in general that does not mean that we should doubt the validity of the
theorems.
[snip]
>> Also, humans read natural language much easier than a
>> formal language, so proofs in English are much easier to read and
>> understand. Most mathematicians prefer understanding a proof themselves
>> over a computer saying that the proof is correct.
>
> Interesting. As a computer scientist we think a lot about what makes
> language both machine-readable and human-readable. One of the design
> goals of XML for example was to do both. It might be possible to come
> up with a language for formal proofs that achieves both goals.
In my personal opinion, the XML people did not a good job in making it
human-readable.
>
> I imagine that many proofs in natural language are hard to read due to
> ambiguities. We have all heard of the term "write only journal". Is
> it possible that there exists a machine-readable formal language that
> may actually *increase* comprehension by humans?
It is possible that such language could exist in the future, but it does
not exist now, to my knowledge. The problem is that in a formal
language, in general you only write what you are doing, and not why you
are doing it.
>
>> Well, first of all, there is no standard format. For exactly the same
>> reason that there is no standard programming language: mathematicians
>> have different requirements, tastes, etc.
>
> Yeah, I thought a bit about this. If we consider the basic rules of
> predicate calculus and FOL as a type of primitive "machine code", and
> we provide a way to define a new notation in terms of that machine
> code - it would be possible to write "notation modules".
>
> "Notation modules" and "formal proofs" could be universally identified
> in a similar way that we do with domain names on the Internet. Once
> named they could be authenticated and uploaded into a distributed
> database.
The problem is not only notational. Also the underlying theory of how
proofs are constructed is different. There are many set theories, type
theories, logics, etc, that you can base a formal proof language on.
groente
-- Sander
Jan Burse
> Well, first of all, there is no standard format. For exactly the same
> reason that there is no standard programming language: mathematicians
> have different requirements, tastes, etc.
>
> groente
> -- Sander
Mizar has its own more natural language oriented format. Example
seen here:
http://lipa.ms.mff.cuni.cz/~urban/xmlmml/html_abstr.930/00mptp_chall_topdown.html
But it seems that this can be readily translated to FOF. For the
MPTP challenge see here:
http://www.cs.miami.edu/~tptp/MPTPChallenge/MPTPChallenge.tgz
(Attention >7MB file)
And FOF might be converted to CNF (Skolemization).
But even if there is a format, the ontology has to be agreed, i.e. do
I use this or that symbol for this or that.
And watch out, the activity of mathematicians might not only consist
of constructing proofs, they might also construct counter models! Or
even use a mixed behaviour:
http://lipa.ms.mff.cuni.cz/~pudlak/publications/sem_an_07.pdf
Constructing counter models is a handy method for disproving things.
Its ultimate justification comes for example from the meta mathematical
result known as Goedels completness theorem:
T |- A iff T |= A
Therefore:
T |/- A iff T |/= A
Therefore
T |/- A iff exists M (M[T u ~A]=1)
Bye
Jan Burse
> Therefore
>
> T |/- A iff exists M (M[T u ~A]=1)
Or does somebody know a way to cast this in a proof
theoretic setting?
Bye
Jan Burse
My guess was once to invent a B, that somehow
characterizes M, and thus have:
T, B |- ~A
But is this a complete disproval method?
Bye
Jan Burse
The problem here is that a trivial solution is B=~A, since:
T, ~A |- ~A.
So we must ask for a B, where T, B is consistent. And for
arithmetic we even don't know whether T is consistent!
Bye
Andrew Tomazos
wrote:
> The problem is not only notational. Also the underlying theory of how
> proofs are constructed is different. There are many set theories, type
> theories, logics, etc, that you can base a formal proof language on.
What are some examples of valid mathematical proofs that use theories/
logics such that any of the following is true:
1. The Theorem Statements cannot be defined in FOL
2. The Axioms on which they are based cannot be defined in FOL
3. The derivation steps from the Axioms to the Theorem cannot be
deduced by FOL.
It was my understanding that all the proofs in mathematical topics
(like abstract algebra, analysis, topology, number theory, probability
and so on) can all be expressed using FOL? (or at least must be able
to if they are correct) and the notations used are just short hand for
FOL statements?
Is this not the case? What is a counterexample?
-Andrew.
Marshall
wrote:
> Andrew Tomazos wrote:
>
> > Interesting. As a computer scientist we think a lot about what makes
> > language both machine-readable and human-readable. One of the design
> > goals of XML for example was to do both. It might be possible to come
> > up with a language for formal proofs that achieves both goals.
>
> In my personal opinion, the XML people did not a good job in making it
> human-readable.
It is an objective fact that the XML people did not do a good
job making it human readable. It is my personal opinion that
they were not competent to do so.
Marshall
A N Niel
<37ea8395-6f7c-46f9...@z5g2000vba.googlegroups.com>,
Andrew Tomazos <and...@tomazos.com> wrote:
Perhaps you will get better answers if you put this in the FOL thread,
not in the computer-verified proof thread.
Jan Burse
> H. J. Sander Bruggink schrieb:
>
>> Well, first of all, there is no standard format. For exactly the same
>> reason that there is no standard programming language: mathematicians
>> have different requirements, tastes, etc.
>>
>> groente
>> -- Sander
>
> Mizar has its own more natural language oriented format. Example
> seen here:
> http://lipa.ms.mff.cuni.cz/~urban/xmlmml/html_abstr.930/00mptp_chall_topdown.html
>
>
> But it seems that this can be readily translated to FOF. For the
> MPTP challenge see here:
> http://www.cs.miami.edu/~tptp/MPTPChallenge/MPTPChallenge.tgz
> (Attention >7MB file)
>
> And FOF might be converted to CNF (Skolemization).
Oops, this would only consist of a format for the premisses
and the conjectures. A format for the proofs itself would
also be needed...
Bye
Marshall
> On 19 June, 09:34, Andrew Tomazos <and...@tomazos.com> wrote:
>
> > If yes, is it also true that all of these deductions could be written
> > in such a way that a computer program can infallibly verify the
> > correctness of these steps?
>
> If the verifier does not contain bugs and runs on top of an
> operating system whose possible bugs will not adversely influence
> the correct functioning of the verifier and both the verifier and
> the operating system run on top of hardware whose possible bugs
> will not adversely influence the correct functioning of the
> verifier and the verifier receives correct input then the answer is
> yes. There are several programmes which do this.
Automated theorem provers are potentially quite complex
and we might realistically worry about bugs there, but
verifiers are quite simple programs. Certainly we should
write them with care, but we shouldn't freak out about
the possibility of error.
Also, programs themselves are subject to proofs of
correctness.
As to hardware and O/S bugs, verifiers read
standard input and write standard output, so
it's not like they are exercising fringe functionality.
It is true that we can never have absolute certainty
that everything is working perfectly, but we shouldn't
let that stop us from things like proof verification.
(Not that you said it should, but you sure didn't make
it sound promising.)
Marshall
Marshall
> which a human reader would immediately pick up but a compiler might
> not. So it is possible that due to such a silly bug in the source
> of a proof the computer will say that a proof is correct when
> actually it is not.
No, that's not what would happen. If the *proof verifier* is
buggy, it might reject a correct proof or accept an incorrect
proof. If the human is confused, he might decide that the
proof said one thing when it really said a different thing.
But the proof itself says what it says, and can't say anything
different from that.
Marshall
H. J. Sander Bruggink
> On Jun 19, 3:10 pm, "H. J. Sander Bruggink" <brugg...@uni-due.de>
> wrote:
>> The problem is not only notational. Also the underlying theory of how
>> proofs are constructed is different. There are many set theories, type
>> theories, logics, etc, that you can base a formal proof language on.
[snip]
> It was my understanding that all the proofs in mathematical topics
> (like abstract algebra, analysis, topology, number theory, probability
> and so on) can all be expressed using FOL? (or at least must be able
> to if they are correct) and the notations used are just short hand for
> FOL statements?
It's certainly true that a large class of mathematical topics can be
represented by first-order logic. But even for first-order logic there
exist various different proof systems. Some like linear Hilbert-style
proofs, some like tree-like Gentzen-style proofs, some like resolution,
etc.
groente
-- Sander
tc...@lsa.umich.edu
Andrew Tomazos <and...@tomazos.com> wrote:
>Furthermore, why isn't there a centralized proof web/database that
>contains all the axioms and verified proofs in some standard format?
People are working on that. An entire issue of the Notices of the American
Mathematical Society was recently devoted to this question.
http://www.ams.org/notices/200811/
Regarding standards, as the old joke goes, the nice thing about standards is
that there are so many to choose from. Mizar is one option, but so is Coq,
Isabelle, HOL Light, ... They all have their pros and cons.
Once you start trying to do this in earnest, you will see that it is not
quite so easy as it might seem at first glance. It's very tedious to write
out a formal proof in full detail, so you need the computer to take some of
the drudgery out of it by filling in the "obvious" steps. This is harder
than it sounds. If you don't believe me, then you should first try your hand
at formalizing a non-trivial theorem in one of the "standard" systems. Then
we can talk.
I'm a fan of going in this direction, but it's more challenging than you
might think.
--
Tim Chow tchow-at-alum-dot-mit-dot-edu
The range of our projectiles---even ... the artillery---however great, will
never exceed four of those miles of which as many thousand separate us from
the center of the earth. ---Galileo, Dialogues Concerning Two New Sciences
tc...@lsa.umich.edu
Andrew Tomazos <and...@tomazos.com> wrote:
>It was my understanding that all the proofs in mathematical topics
>(like abstract algebra, analysis, topology, number theory, probability
>and so on) can all be expressed using FOL? (or at least must be able
>to if they are correct)
You should really say that everything can be expressed in the first-order
language of set theory, and proved in ZFC. But morally speaking what you
say here is correct, with only minor caveats. (One such caveat: FOL is
*classical* logic, and people who accept only intuitionistic logic won't
like some of your FOL proofs.)
>and the notations used are just short hand for FOL statements?
This is a lot more debatable. Just because a mathematical statement *can*
be formalized set-theoretically and proved from the axioms of ZFC doesn't
mean that it's "just shorthand" for the formal statement. The point is
that the statement can also be formalized in different ways. If the argument
is sufficiently constructive, it can also be formalized in intuitionistic
logic. In that case, is the argument shorthand for the classical formal
proof or the intuitionistic formal proof?
Lots of statements can be formalized in first-order arithmetic and proved
from the first-order Peano axioms. Are the statements then shorthand for
formal theorems of ZFC or are they shorthand for formal theorems of PA?
Even if you stick to classical logic, you might be interested in just how
strong a set of axioms you need to prove your theorem. It is interesting
to know that the Paris-Harrington theorem is provable in ZFC but not in PA.
So you don't necessarily want to think of a mathematical theorem like the
Brouwer fixed-point theorem as a unique formal entity in a unique formal
system, because then you might not be able to easily answer questions about
which axioms are really necessary for proving your theorem.
Jan Burse
> If the argument is sufficiently constructive, it can also be formalized in
> intuitionistic logic. In that case, is the argument shorthand for
> the classical formal proof or the intuitionistic formal proof?
Depending on your intuitionistic set up, not much is gained. An
intuitionistic proof might just be a normal classical proof, that
doesn't use for example the following axiom schema:
--------
A v ~A
So you might have a verifier, and proof automation tools, etc.. that
simultaneously support classical and intuitionistic logic. About
the differences in quantifiers I am not so sure.
Also a class of the available systems is agnostic about whether you
work with classical or intutionistic logic. They are based on some
minimal logic, and classical respective intuitionistic logic is based
on a module that is loaded.
Bye
Jan Burse
> tc...@lsa.umich.edu schrieb:
>> If the argument is sufficiently constructive, it can also be
>> formalized in
> > intuitionistic logic. In that case, is the argument shorthand for
>> the classical formal proof or the intuitionistic formal proof?
>
> Depending on your intuitionistic set up, not much is gained. An
> intuitionistic proof might just be a normal classical proof, that
> doesn't use for example the following axiom schema:
Whereby the relationship of intuitionistic and classical
is that of a containment, there is also relationship
between hilbert style proofs and natural deduction style
proofs.
You can convert in both directions, and by the curry
howard isomorphism, there is an analogy in combinator
calculus/lambda calculus.
I am not so sure what role verifiers or automated proof
tools will play here. Again given a sufficient minimal
logic, both can coexist in the proof system...
Bye
Patricia Shanahan
...
> Once you start trying to do this in earnest, you will see that it is not
> quite so easy as it might seem at first glance. It's very tedious to write
> out a formal proof in full detail, so you need the computer to take some of
> the drudgery out of it by filling in the "obvious" steps. This is harder
> than it sounds. If you don't believe me, then you should first try your hand
> at formalizing a non-trivial theorem in one of the "standard" systems. Then
> we can talk.
Although proofs and computer programs are different things, I see some
analogies.
A formal proof in full detail is something like an assembly language
program. Humans can, in practice, only write very short assembly
language programs, and tend to make mistakes when doing so.
Traditional proofs, as they appear in mathematics papers, are something
like algorithms in pseudo-code. They are easier for people to write and
understand, but not good as computer input.
A lot of research in computer science has been about constructing
languages that can be mapped to assembly language, or equivalent, by a
compiler but that are easier for people to read and write. High level
programming languages combine abstraction, reuse, and modularization,
but keep formality.
Has there been a similar trend in proof languages?
Patricia
LudovicoVan
> series of well-defined logical deductions from some set of axioms and
> rules?
>
> in such a way that a computer program can infallibly verify the
> correctness of these steps?
Wasn't that the so called Hilbert's program?
I wouldn't think the difficulties are just technical (in the strict
sense).
-LV
Andrew Tomazos
> >It was my understanding that all the proofs in mathematical topics
> >(like abstract algebra, analysis, topology, number theory, probability
> >and so on) can all be expressed using FOL? (or at least must be able
> >to if they are correct)
>
> You should really say that everything can be expressed in the first-order
> language of set theory, and proved in ZFC. But morally speaking what you
> say here is correct, with only minor caveats. (One such caveat: FOL is
> *classical* logic, and people who accept only intuitionistic logic won't
> like some of your FOL proofs.)
Ok, so perhaps something more primitive is required for the atomic
basis of the formal language in which the theorems, axioms and proofs
are expressed.
Perhaps if we provide a "machine code" in which one can define any
propositional calculus it would provide sufficiently general building
blocks such that one can express the axioms of FOL, ZFC,
intuitionistic logic, Peano axioms and so forth. Perhaps there would
be competing versions of these different modules in the database, and
it would be up to each mathematician to choose which to build on.
It would also be interesting to perform a dependency analysis as you
say to see which axioms were actually used to prove theorem X. In
reality there is no such thing as an absolute theorem. All theorems
are in fact only theorems in the relative context of which axioms they
need. I can prove any theorem X by simply making X an axiom. :)
-Andrew.
tc...@lsa.umich.edu
Jan Burse <janb...@fastmail.fm> wrote:
>So you might have a verifier, and proof automation tools, etc.. that
>simultaneously support classical and intuitionistic logic. About
>the differences in quantifiers I am not so sure.
One issue, which may be more of a data management issue than a fundamental
problem, is that intuitionistically you will want to separately track
the two statements "set S is not infinite" and "set S is finite" (e.g.,
if the former is a known theorem while the latter is still conjectural),
whereas classically there is no distinction. The classical user might
be confused that "set S is finite" is marked as a conjecture.
Andrew Tomazos
> Has there been a similar trend in proof languages?
Here is a list of the proof languages that I've just mined for
investigation:
- Boyer-Moore
- Mizar
- Coq
- Isabelle
- HOL Light
So far all of them exhibit the relentless dedication to user-
friendliness that we have come to expect from software projects out of
academia. :) (Any time you get a Software Engineering Process book or
a HCI book from an author that has never left their university campus
- burn it.)
-Andrew.
LudovicoVan
> I can prove any theorem X by simply making X an axiom.
Right, but there is soundness, not only validity... I.e. there is an
underlying problem of "meaning" which, AFAIK, cannot really be
formalised (in this sense, any formalisation is a reduction to an
abstract game, just meaningless when taken on its own).
-LV
Andrew Tomazos
If it can't be formalized than does it have a place in mathematics?
Or, put another way - what is an example of something in mathematics
that has meaning but can't be formalized?
-Andrew.
Herman Rubin
Andrew Tomazos <and...@tomazos.com> wrote:
>Is it true that all proofs of mathematical theorems must contain a
>series of well-defined logical deductions from some set of axioms and
>rules?
>If yes, is it also true that all of these deductions could be written
>in such a way that a computer program can infallibly verify the
>correctness of these steps?
>If also yes, than why isn't it required that the centerpiece of any
>published proof be the "source code" for such a computer verification?
>ie Shouldn't the center of every proof be a machine-readable theorem
>and machine-readable steps to undeniably deduce that theorem? The
>English should just be annotation essentially.
The problem is that at the present time these proofs,
written in computerese, would be too long. For some
of them, the proof, in "natural deduction", might be
only about three to five times the length of the
present proofs.
Most of the present proofs are close enough to formal
to be verified by people. Computers are superfast
subimbeciles, and need to be instructed most carefully,
which is too carefully for reasonable length papers.
However, there are theorems for which a computer was
carefully instructed to go through all the steps necessary,
and for which we do not have a reasonably human readable
version of the proof.
>Furthermore, why isn't there a centralized proof web/database that
>contains all the axioms and verified proofs in some standard format?
>If we had some standard naming reservation system than you could use
>an old theorem from one verified proof in the database as a "basis
>axiom" for a new proof.
>What am I missing?
> -Andrew.
We do not have a standard language. One can add macros to
the computer proof; for example, in the basic language, one
would have to prove e_1 = e_2, e_2 = e_3, ..., while one
normally writes e_1 = e_2 = e_3 ... , usually leaving out
the explicit description of the step. For example, proving
the associative law for addition from the Peano Postulates,
one now does
(a +b) + 0 = a+b = a+(b+0)
if (a+b)+c = a+(b+c), then
(a+b)+c' = ((a+b)+c)' = (a+(b+c))'
= a+(b+c)' = a+(b+c')
Then (a+b)+c = a+(b+c) by induction and universal generalization
Now how would this have to be done in a computer formal proof?
1 (a+b)+0 = a+b definition of addition of 0
2 b = b+0 definition of addition of 0
3 a+b = a+(b+0) substitution of equals
4 (a+b)+0 = a+(b+0) 1, 3, transitivity of =
I will leave out the rest; as you can see, the proofs
get lengthy.
If we have something like, "in a similar manner", the whole
thing would have to be repeated. People can think; computers
can only carry out instructions.
While it is true that any theorem has a completely computer
verified formal proof, and possibly some should have a more
formal proof "published", as of yet it generally takes too
much work to even produce the formal proof.
--
This address is for information only. I do not claim that these views
are those of the Statistics Department or of Purdue University.
Herman Rubin, Department of Statistics, Purdue University
hru...@stat.purdue.edu Phone: (765)494-6054 FAX: (765)494-0558
Andrew Tomazos
> >So you might have a verifier, and proof automation tools, etc.. that
> >simultaneously support classical and intuitionistic logic. About
> >the differences in quantifiers I am not so sure.
>
> One issue, which may be more of a data management issue than a fundamental
> problem, is that intuitionistically you will want to separately track
> the two statements "set S is not infinite" and "set S is finite" (e.g.,
> if the former is a known theorem while the latter is still conjectural),
> whereas classically there is no distinction. The classical user might
> be confused that "set S is finite" is marked as a conjecture.
Well this would be a question of which module you import:
import intuitionistic_logic
or
import classical_logic
If you depend on "set S is finite" and changed between them then your
proof would no longer verify.
-Andrew.
Herman Rubin
Andrew Tomazos <and...@tomazos.com> wrote:
>On Jun 19, 11:44=A0am, William Elliot <ma...@rdrop.remove.com> wrote:
<> > If also yes, than why isn't it required that the centerpiece of any
<> > published proof be the "source code" for such a computer verification?
<> Because it would be necessary to prove that the code had no errors.
>This is a completely illogical position. A proof must be published in
>some language. Currently most are published in a mix of natural
>language and mathematical notation. Is it necessary to prove that the
>humans that read and approve these proofs contain no errors before
>making them theorems? Of course not.
>What I am suggesting is that we specify a standard language that all
>mathematical proofs are written in, that both humans and computers can
>read and verify. It seems this is exactly what Mizar is. It seems as
>though if we did this it would be far quicker and more rigorous than
>what we do now. It also seems like the basic rules of transformation
>from one statement to another are so simple, that any bugs contained
>in verifier implementations would quickly and easily be eradicated.
<> Principia Mathematica, by Burtran Russel was a large three volume
<> work that did no more than prove the very basics of logic and set theory.
<> Upon publication, besides the usually errata, it was found to have fatal
<> flaws.
>Exactly my point. If "Principia Mathematica" was written in machine-
>readable format, than the verifier software would of caught these
>errors wouldn't it?
> -Andrew.
Not necessarily. One could cite an incorrect formulation,
and the verifier would accept this; otherwise, one might
have to redefine addition in every number theory proof.
MoeBlee
> On 19 June, 09:34, Andrew Tomazos <and...@tomazos.com> wrote:
>
> > Is it true that all proofs of mathematical theorems must contain a
> > series of well-defined logical deductions from some set of axioms and
> > rules?
>
> > If yes, is it also true that all of these deductions could be written
> > in such a way that a computer program can infallibly verify the
> > correctness of these steps?
>
> Wasn't that the so called Hilbert's program?
The claim that all mathematical proofs are in principle formalizable
is sometimes called 'Hilbert's thesis', and that is an important part
of the idea behind Hilbert's program. However, also central to
Hilbert's program is finding an axiomatization of mathematics and
finding a finitary proof of the consistency of that axiomatization.
MoeBlee
Jan Burse
> In article <h1gdqf$2uv$1...@news.albasani.net>,
> Jan Burse <janb...@fastmail.fm> wrote:
>> So you might have a verifier, and proof automation tools, etc.. that
>> simultaneously support classical and intuitionistic logic. About
>> the differences in quantifiers I am not so sure.
>
> One issue, which may be more of a data management issue than a fundamental
> problem, is that intuitionistically you will want to separately track
> the two statements "set S is not infinite" and "set S is finite" (e.g.,
> if the former is a known theorem while the latter is still conjectural),
> whereas classically there is no distinction. The classical user might
> be confused that "set S is finite" is marked as a conjecture.
Thanks, interesting point. Does this mean that the classical and
intuitionistic ontology is different? Maybe yes, the vocabulary
can be the same, I can also form an antonym in intuitionistic
logic, but some inferences are lacking, like double negation.
Bye
tc...@lsa.umich.edu
Patricia Shanahan <pa...@acm.org> wrote:
>A lot of research in computer science has been about constructing
>languages that can be mapped to assembly language, or equivalent, by a
>compiler but that are easier for people to read and write. High level
>programming languages combine abstraction, reuse, and modularization,
>but keep formality.
>
>Has there been a similar trend in proof languages?
Yes, certainly. All the standard languages are high-level in your sense.
Here's a comparison between two of them, from Freek Wiedijk's article in
the Notices of the AMS that I pointed to earlier:
The main advantage of HOL Light is its elegant architecture,
which makes it a very powerful and reliable system. A proof of
the correctness of the 394 line HOL Light "logical core" even has
been formalized. On the other hand HOL has the disadvantage that it
sometimes cannot express abstract mathematics---mostly when it involves
algebraic structures---in an attractive way. It *can* essentially
express all abstract mathematics though. Another disadvantage of HOL
is that the proof parts of the HOL scripts are unreadable. They can
only be understood by executing them on the computer.
Mizar on the other hand allows one to write abstract mathematics
very elegantly, and its scripts are almost readable like ordinary
mathematics. Also Mizar has by *far* the largest library of already
formalized mathematics (currently it is over 2 million lines).
However, Mizar has the disadvantage that it is not possible for a
user to automate recurring proof patterns, and the proof automation
provided by the system itself is rather basic. Also, in Mizar it is
difficult to express the formulas of calculus in a recognizable style.
It is not possible to "bind" variables, which causes expressions
for constructions like sums, limits, derivatives, and integrals to
look unnatural.
Here's some sample code, again from Wiedijk's article. First, HOL Light:
let CONG_MINUS1_SQUARE = prove
('2 <= p ==> ((p - 1) * (p - 1) == 1) (mod p)',
SIMP_TAC[LE_EXISTS; LEFT_IMP_EXISTS_THM] THEN
REPEAT STRIP_TAC THEN
REWRITE_TAC[cong; nat_mod;
ARITH_RULE '(2 + x) - 1 = x + 1'] THEN
MAP_EVERY EXISTS_TAC ['0'; 'd:num'] THEN
ARITH_TAC);;
And now Mizar:
theorem Th11:
i gcd m = 1 & i is_quadratic_residue_mod m &
i,j are_congruent_mod m
implies j is_quadratic_residue_mod m
proof
assume
A1: i gcd m = 1 &
i is_quadratic_residue_mod m &
i,j are_congruent_mod m;
then consider x being Integer such that
A2: (x^2 - i) mod m = 0 by Def2;
m divides (i - j) by A1,INT_2:19;
then
A3: (i - j) mod m = 0 by Lm1;
(x^2 - j) mod m
= ((x^2 - i) + (i - j)) mod m
.= (((x^2 - i) mod m) + ((i - j) mod m))
mod m by INT_3:14
.= 0 by A2,A3,INT_3:13;
hence thesis by Def2;
end;
tc...@lsa.umich.edu
Herman Rubin <hru...@odds.stat.purdue.edu> wrote:
>While it is true that any theorem has a completely computer
>verified formal proof, and possibly some should have a more
>formal proof "published", as of yet it generally takes too
>much work to even produce the formal proof.
Too much work for the average mathematician, yes. But too much work for
someone with an interest in the subject, no. See for example
http://www.cs.ru.nl/~freek/100
for a list of theorems that have been fully formalized.
Jan Burse
Looks like somebody is comparing apples and oranges.
It seams the the HOL light stuff is a tactic. Whereas
the mizar snippet is a thereom.
What is a tactic, the same as a theorem?
I don't think so. A tactic is a proof method, and
the HOL light code might show the invocation of a
proof method. The proof method will in the end
produce a proof.
Only if you run the HOL light stuff you will get
a proof, and then you can compare this with the mizar
stuff. But comparing the tactic invocation and the
mizar proof looks to me unfair.
Bye
pubkeybreaker
> In article <h1gj84$3...@odds.stat.purdue.edu>,
>
>
> http://www.cs.ru.nl/~freek/100
>
> for a list of theorems that have been fully formalized.
Impressive list. PNT surprised me, as did a number of others.
Anyone up to tacking the classification theorem? :-) :-)
tc...@lsa.umich.edu
Andrew Tomazos <and...@tomazos.com> wrote:
>Well this would be a question of which module you import:
>
> import intuitionistic_logic
>
>or
>
> import classical_logic
>
>If you depend on "set S is finite" and changed between them then your
>proof would no longer verify.
As I said, I don't think the obstacle is *fundamental* here, but I also
believe that you're underestimating the data management problems.
What you wrote above makes it sound like we have a single database of formal
statements, all expressed in a single language, and depending on which logic
we want, some will come out as theorems and some won't.
In reality, things are not that simple, because classically there will
be some objects whose existence has been classically proven, but not
intuitionistically proven. Classically, you'll want to introduce *names*
for some of those objects so that you can refer to them. But then do we
mark any statement involving that name intuitionistically conjectural?
Some such statements might in fact be intuitionistically proven, but by
some means that bypasses the classically proven but intuitionistically
suspect lemma.
Again, I think that your best bet at this stage is to move from armchair
theorizing to learning one or more of the standard systems that are already
out there. Read the Notices of the AMS issue I pointed to, and start
learning how to use Mizar or HOL Light.
Andrew Tomazos
> (a +b) + 0 = a+b = a+(b+0)
>
> if (a+b)+c = a+(b+c), then
> (a+b)+c' = ((a+b)+c)' = (a+(b+c))'
> = a+(b+c)' = a+(b+c')
It's an interesting example.
So the question is given something like "(a+b)+c'" = "((a+b)+c)'" and
the huge list of axioms and results, can the computer deduce which one
you used to perform this step?
Or would you necessarily have to tell it that "I'm using axiom (x+y')
= ((x+y)') where x = (a+b) and y = c."
In this specific case I can imagine creating a parse tree of both
sides and then performing some kind of diff algorithm against them.
Then factor out the common parts into a pattern, and then searching
the axiom list for that pattern.
Perhaps there would be a way to bind this in realtime with some kind
of auto completion feature (like intellisense) in the editor
software. Maybe it could make a guess and provide a short-list in a
menu for you to select, to remove some of the tedium.
Once the explanation step has determined it doesn't necessarily be
displayed inline at that point, perhaps it can be linked to a second
longer file that is published like an appendix.
As Patricia Shanahan pointed out, we already have built up many
tactics to manage this sort of complexity in computer programming.
-Andrew.
tc...@lsa.umich.edu
LudovicoVan <ju...@diegidio.name> wrote:
>Right, but there is soundness, not only validity... I.e. there is an
>underlying problem of "meaning" which, AFAIK, cannot really be
>formalised (in this sense, any formalisation is a reduction to an
>abstract game, just meaningless when taken on its own).
It's true that there are problems with formalizing meaning. However, that
isn't necessarily an obstacle to delegating the verification of proofs to
a computer. As human users we still have to agree that the formal theorem
that we give the computer to verify adequately expresses what we have in
mind. But given that, the computer can check the correctness of any proof
we offer for the theorem, without having to know what we mean by the theorem.
tc...@lsa.umich.edu
Jan Burse <janb...@fastmail.fm> wrote:
>What is a tactic, the same as a theorem?
>
>I don't think so. A tactic is a proof method, and
>the HOL light code might show the invocation of a
>proof method. The proof method will in the end
>produce a proof.
>
>Only if you run the HOL light stuff you will get
>a proof, and then you can compare this with the mizar
>stuff. But comparing the tactic invocation and the
>mizar proof looks to me unfair.
It depends on what you are trying to compare. If you are trying to compare
what a human being has to type into the computer to get a formal proof "out
the other end" so to speak, then the comparison is fair.
On the other hand, it is true that HOL Light and Mizar have different
underlying philosophies, so you could say that they are apples and oranges.
For a start, Mizar is based on a ZFC-like system, whereas HOL Light is based
on higher-order logic. More relevantly here, HOL Light relies heavily on a
tactic-based approach; in practice, almost all proofs are generated via
tactics rather than by "typing them in directly" so to speak. This is a
very powerful approach, but it does require thinking about proofs in a
slightly different way from what we're used to.
Jan Burse
> In reality, things are not that simple, because classically there will
> be some objects whose existence has been classically proven, but not
> intuitionistically proven. Classically, you'll want to introduce *names*
> for some of those objects so that you can refer to them. But then do we
> mark any statement involving that name intuitionistically conjectural?
> Some such statements might in fact be intuitionistically proven, but by
> some means that bypasses the classically proven but intuitionistically
> suspect lemma.
Interesting approach. Marking theorems as either intuitionistic
or classical. And when then subsequent theorems are formed, all
based on intuitionistic theorems and by intuitionistic rules, we
have again an intuitionistic theorem.
One simple problem is here. A theorem might have different competing
proofs. This cries for multi marking! Or a theorem might have a
classical proof right now, but later we will find an intuitionistic
proof. This cries for the revision of markings!
Anyway, I saw, that for example in metamath, competing proofs are
there, but they have each individual identifiers. And only in the
free text comment section of a theorem, such relationships between
theorems are found.
Bye
tc...@lsa.umich.edu
pubkeybreaker <pubkey...@aol.com> wrote:
>Impressive list. PNT surprised me, as did a number of others.
Yes, I remember being very impressed when Avigad announced his proof.
FYI, it turned out that the Erdos-Selberg elementary proof was very helpful
here. The complex-analytic proof is quite a bit more cumbersome because you
need to develop the complex-analytic machinery along the way. I'm not sure
which proof the HOL Light proof is based on.
>Anyone up to tacking the classification theorem? :-) :-)
I'd be happy just to live to see the completion of the GLS project!
Jan Burse
> More relevantly here, HOL Light relies heavily on a tactic-based approach;
> in practice, almost all proofs are generated via tactics rather
> than by "typing them in directly" so to speak. This is a very powerful
> approach, but it does require thinking about proofs in a
> slightly different way from what we're used to.
I don't see a reason to have it like that because of the
underlying logic substrate. What is the motivation? I think
some nuances will get lost. For example it will not be possible
to use the system to try to most literally translate existing
proofs.
Bye
Jan Burse
> I don't see a reason to have it like that because of the
> underlying logic substrate. What is the motivation? I think
> some nuances will get lost. For example it will not be possible
> to use the system to try to most literally translate existing
> proofs.
>
> Bye
Except by using a bunch of constructor tactics. Given the literal
translation requirement, we see that the length of a proof
is not a measure for a proof verification system. More its
versatility.
Best Regards
tc...@lsa.umich.edu
Jan Burse <janb...@fastmail.fm> wrote:
[Re: HOL Light tactics]
>I don't see a reason to have it like that because of the
>underlying logic substrate. What is the motivation?
The motivation is that producing a formal proof is, to a great extent,
mind-numbingly tedious. We want the computer to do as much of that work
automatically as we can. Proof tactics are a powerful way to automate
formal proof production. The higher-order logic also allows one to
automate recurring proof "patterns."
>I think some nuances will get lost. For example it will not be possible
>to use the system to try to most literally translate existing proofs.
This is true, but let me ask, is the real purpose of the database of formal
proofs to *literally translate existing proofs*, or to *verify correctness*?
My philosophy is the latter. I see the computer's role as checking that
alleged theorems are really theorems. I don't really care if the computer's
proof is not quite the same as the argument I give to my fellow human beings
to get them to understand the proof.
This is the philosophy followed by most of the leaders in the theorem-proving
community. When Gonthier formalized the four-color theorem in Coq, he found
himself coming up with new ideas in order to make the proof easier to feed
to the computer. Thus his proof is by no means a literally faithful
rendition of the pre-existing human proofs.
If you see "literal translation" as an important goal, then I agree that
you'll need to come up with some approach that is different from the existing
ones. I personally don't see that literal translation is that important.
Jan Burse
> If you see "literal translation" as an important goal, then I agree that
> you'll need to come up with some approach that is different from the existing
> ones. I personally don't see that literal translation is that important.
Many times the journey is the reward. I doubt that many theorems are
useful in itself. They are often simplifications or culminations of
a set of subtheorems and lemmas which have much more substance as the
theorem itself.
Take for example a completness theorem. Not so exiting in itself.
But if we take a Henkin proof of it, we see a total new world, with
a lot of subcorollaries. And a Gï¿œdel proof of the same theorem
might look totally different.
I agree at the moment the automated theorem prooving community
resembles more a world cup organization. They make competitions
and what counts is the number of theorems proved and the time
taken to proof the theorems.
Fine. But do we judge a mathematician by the time it took him to
produce a proof. Or do we judge him by some properties the proof
exhibits?
Bye
Jan Burse
> Fine. But do we judge a mathematician by the time it took him to
> produce a proof. Or do we judge him by some properties the proof
> exhibits?
>
> Bye
http://en.wikipedia.org/wiki/Paul_Erd%C5%91s
He had his own idiosyncratic vocabulary: he spoke of “The Book”, an
imaginary book in which God had written down the best and most elegant
proofs for mathematical theorems. Lecturing in 1985 he said, “You don’t
have to believe in God, but you should believe in The Book.” He himself
doubted the existence of God, whom he called the “Supreme Fascist”
(SF).[9] He accused the SF of hiding his socks and Hungarian passports,
and of keeping the most elegant mathematical proofs to himself. When he
saw a particularly beautiful mathematical proof he would exclaim, “This
one’s from The Book!”. This later inspired a book entitled Proofs from
THE BOOK.
Victor Porton
Mizar and maybe Isabelle is more flexible and powerful that Mizar.
(I'm not an expert in this however.)
tc...@lsa.umich.edu
Jan Burse <janb...@fastmail.fm> wrote:
>Fine. But do we judge a mathematician by the time it took him to
>produce a proof. Or do we judge him by some properties the proof exhibits?
I think you're conflating two different issues here.
The first issue is whether proofs---in the ordinary sense of the word, not
formal proofs---have inherent value or beauty, beyond doing their job of
establishing the correctness of a theorem. Here we have no disagreement.
Important theorems should ideally be proved in many different ways, each
one giving new insight into what is going on. Proofs do more than certify
correctness; they can *explain* a result, suggest new conjectures, introduce
new and powerful general techniques that can be used to solve other problems,
and so on.
The second issue, which is very different from the first, is whether *formal*
proofs should *literally translate* pre-existing ordinary proofs. I don't
really see the point of this. Formal proofs are far inferior to proofs
written in natural language when it comes to readability; I would not turn
to a formal proof to understand *why* the prime number theorem is true.
Ordinary proofs, written in natural language, have served and will continue
to serve the function of transmitting mathematical knowledge from one human
being to another, far better than formal proofs ever will.
The one area where formal proofs have a decisive advantage over natural-
language proofs is correctness. It therefore makes a lot of sense to use
formal proofs to carry out the function of certifying correctness. But for
this purpose, slavish imitation of ordinary proofs is not necessary, and
can indeed be an impediment.
To repeat, I have not seen you give any good argument for why *formal* proofs
should *literally translate* natural-language proofs.
MeAmI.org
End it.
In general, researchers believe P does not equal NP, because ever
since 1971, the mathematical basis of the algorithm remains supportive
of the intended purpose.
We have a contradiction. The set of Goedel-formulas of PA is empty,
and PA has no non-standard models.
I tell you the truth, Computional Theory contains all the axioms and
verified proofs in some standard format.
Do the math.
It's human nature.
Stephen Arthur Cook had a purpose with P Versus NP. Did it serve you?
It did not serve me.
Perhaps it served institutional investors in the S&P?
1. There is a reason Intel labs at Berkeley: to make money.
2. There is a reason Berkeley hosts Intel: to make money.
The overlap between innovation and academia is self-evident and
important to commerce.
This does not make Intel or Berkeley guilty of anything. I am simply
establishing a symbiosis of reason.
I tell you the truth, Cryptography can and is continually abused.
Why did Wall Street recede and the economy decline?
Because those in a position to leverage information pushed the
envelope past reason.
Their actions escaped capitalism and as a class bordered oligopoly.
Consider the anti-virus industry? Does it seve you? We are told to
fear understanding computation outside of sanctioned languages and
those who do seek this understanding are labeled as troublemakers.
Anything Microsoft does not want you to use they can call a virus.
Read the "Terms of Service" on your Windows OS.
The record speaks:
The Cornficker hype peaked investors in the parent company made $10
million dollars with the Dow down 200+ points.
It does not serve me. Perhaps it served institutional investors in the
S&P?
Suppose that p and p+2 are both prime and that there are the biggest
pair IF P = NP then problems like the subset-sum problem are as "easy"
to Proof as to compute.
IF P = NP then problems like the subset-sum problem are as "easy" a
discussion on USENET.
Assume P=NP. Let y be a proof that P=NP. The proof y can be verified
by computer scientists to produce a proof).
P, NP and mathematics – a computational complexity perspective
enabling the computer revolution, made mathematically precise what
Hilbert predicted.
+++
(Facts)
+
1. The correct solution to the search problem can be easily verified
by V.
2. The extension of standard NP proofs was suggested "independently"
in two academic publications.
3. Smale: "Mathematical problems for the next century, Mathematical
Intelligencer" [...]. The "standard cryptographic" conjecture (about
the existence of hard [problems] [...] The lengths of proofs, in:
Handbook of Proof Theory, ed. [...] Proof Verification and
Approximation Algorithms Lecture Notes in Computer Science, Vol.
1367.http://www.math.cas.cz/~krajicek/pnp_syll.html
4. P=NP Proof Published at CERN (Musatov)[...]"standard practice when
using Quick Sort to make it effective for faster convergence.). [....]
(NP/P) . This is true since the speed of the Computer should not be
[deterministic].
It can be empirically verified as follows.
A. If n is the numerical [....] (sci.math); Re: Perfection in Proof:
Please Critique! [...] P) algorithm results [...]http://sci.tech-
archive.net/Archive/sci.math/2009-05/msg01035.html
B. Scott Aaronson (MIT)
Shtetl-Optimized » Blog Archive » A far-off dream: automating a [...]
25 Aug 2006 [...] Were it standard to present proofs in computer-
checkable form, [....] Its main point is that math is verified [....].
That, to me, is why P vs. NP is one of the most profound questions
that humans have ever asked. [...].
http://scottaaronson.com/blog/%3Fp%3D116
PRIMES is in P little FAQ 25 Oct 2004 [...] Time here is not defined
in seconds, nor in computer cycles of a [...].
An equivalent, and now standard, way of viewing problems that are in
NP is to say that a [...] A mathematical proof demonstrating whether P
is equal to NP or not is [....] an integer is prime, which can be
verified in polynomial time).
P=NP.
qed
¤
•
.
Michel Hack
> A formal proof in full detail is something like an assembly language
> program. Humans can, in practice, only write very short assembly
> language programs, and tend to make mistakes when doing so.
>
> Traditional proofs, as they appear in mathematics papers, are something
> like algorithms in pseudo-code. They are easier for people to write and
> understand, but not good as computer input.
The translation of pseudo-code, or of a high-level language by a
compiler,
to something like assembly language typically changes the size of the
code
by a linear factor, except possibly in cases of recursive macro
expansions
(that, in practice, would blow the compiler's storage allocation).
Translating a traditional math proof to a formal proof often involves
an
exponential explosion in size, and sometimes MUCH worse (Ackermann-
like).
That is because definitions have to be expanded, and some definitions
may
be recursive or even doubly-recursive. A lot depends on the notation
of
course: if the formal system only has the successor notation for
numerals
the exponential explosion is almost guaranteed.
Now, perhaps there are automatic verifiers that can handle
transformations
whose validity has been proved separately -- but was THAT proof
formal?
Those kinds of proof are often of the kind that explodes in size.
Michel.
Jan Burse
> .
fuck off
Jan Burse
> Ordinary proofs, written in natural language, have served and will continue
> to serve the function of transmitting mathematical knowledge from one human
> being to another, far better than formal proofs ever will.
The greeks believed at some point that written books are evil
since spoken transmition is far superior.
I can't believe the argument you are giving. It sounds like since
formalized proofs are not readable now, we should not work in the
direction of improving the readability. So you are making the alleged
status quo as the future goal.
First of all that formalized proofs are not readable, is this juts
gut feeling of yours, or is this based on real experience? I recently
tried to read a computer formatted formal mizar article. And it was
quite good readable. What do you think are programmers doing all day
when they are not writing code? They might read others code...
Its just a matter of education and improved tools and artificial
languages, but it is not an argument as you think. It is not an
impossibilty to work in formal systems. Its already day to day
reality for many peoples. For example 2006 there were around
13.3 million professional developers world wide.
http://www.theserverside.com/discussions/thread.tss?thread_id=18838
And they might do business model formalizations, they write
code for requirements. Struggling with a lot of validation and
verification issues. Some verification techniques could be
of great help.
Bye
Andrew Tomazos
> > > Interesting. As a computer scientist we think a lot about what makes
> > > language both machine-readable and human-readable. One of the design
> > > goals of XML for example was to do both. It might be possible to come
> > > up with a language for formal proofs that achieves both goals.
>
> > In my personal opinion, the XML people did not a good job in making it
> > human-readable.
>
> It is an objective fact that the XML people did not do a good
> job making it human readable. It is my personal opinion that
> they were not competent to do so.
Every web site of the 40 Petrabytes (40,000 GB) that are currently
online are written in HTML as a base, which is essentially an
application of XML (technically they both descend from SGML).
Clearly, regardless of the W3Cs alleged incompetence, one cannot argue
that it is a virtually universal language that both humans and
machines parse.
I'm not suggesting that the ideal formal proof language would look
like XML. I imagine it would look as similar to current proofs as
possible while (a) making the minimum changes to make it both machine-
readable and machine-verifiable; and (b) taking advantage of computer-
aided features not available in static natural language.
Eventually the ability of the verification algorithms are going to get
better at deducing how to get from some well-formed formula X to some
other well-formed formula Y based on the large set of available
premises. This is essentially what mathematicians are "good at" when
reading a proof that omits some of these steps.
When that happens the formal language proofs will become shorter and
eventually approach (or even surpass) the natural language proofs. I
imagine in 50 years time, all mathematicians will be working in a
formal language in an IDE, not because they are interested in more
correctness - simply because it will be easier to have the computer at
your side, and will speed up research.
We could in fact get there today, but all the systems (Mizar, HOL,
Isabelle, etc) have had so little investment - and so few experienced
developers work on them. Basically there isn't the impetus or money
to make it happen quickly, probably because most mathematicians do not
yet appreciate the potential benefit to their productivity.
-Andrew.
Andrew Tomazos
> >Well this would be a question of which module you import:
>
> > import intuitionistic_logic
>
> >or
>
> > import classical_logic
>
> >If you depend on "set S is finite" and changed between them then your
> >proof would no longer verify.
>
> statements, all expressed in a single language, and depending on which logic
> we want, some will come out as theorems and some won't.
>
> In reality, things are not that simple, because classically there will
> be some objects whose existence has been classically proven, but not
> intuitionistically proven. Classically, you'll want to introduce *names*
> for some of those objects so that you can refer to them. But then do we
> mark any statement involving that name intuitionistically conjectural?
Here is a more detailed explanation of what I was imagining with
respect to the "data management" issues as you call them.
The basic system works on compilation units, which are individual
files.
Within a compilation unit you may:
(a) define a propositional calculus
(b) define aliases, names and truth-preserving rules based on previous
ones
(c) state axioms
(d) make statements (which must deducibly true from previous
statements, axioms and rules)
(e) import other compilation units
Each compilation unit has its own namespace, and names from one
compilation unit can be selectively imported into another.
There is some central registry where individuals and organizations can
register their identity and get a key to sign the compilation units
they produce. (Perhaps reusing the Internet domain name system as a
basis.)
So for example the math department at MIT might register the name
"edu.mit" and create a compilation unit in which they define what they
consider to be the foundation of intuitionistic logic as
"edu.mit.intuit_logic".
Once signed these compilation units can be distributed and copied in
whatever manner the author sees fit. There is no need for
centralization of anything other than the signing authority.
You may then create a new compilation unit that imports some objects
and names from the "edu.mit.intuit_logic" into your compilation unit.
Because all the compilation units are universally named and signed,
the object "edu.mit.intuit_logic.infinite_set" is also uniquely
defined.
This means that the system is agnostic to the specific names for
things. What you consider to be a "lattice" is bound to either (a)
what you defined it to be or (b) the definition you endorsed by
importing it into your compilation unit.
When a compilation unit is verified, the machine will first check that
all the language is well-formed, then it will check that all the
statements are true, and then if successful, output a summarizable
report of the axioms and truth-preserving rules that were used to
determine the truth of each statement.
When published this output could be included as an appendix in the
compilation unit, in a similar way as when a programmer shows the
output of a program after the source code.
How does this description of naming fit into the concerns you stated
regarding objects that are conjectural in intuitionistic logic but
proven in classical logic? This isn't clear to me.
-Andrew.
LudovicoVan
> In article <c7f29cec-fd13-4ccb-8fee-63b2d7536...@r3g2000vbp.googlegroups.com>,
>
> LudovicoVan <ju...@diegidio.name> wrote:
> >Right, but there is soundness, not only validity... I.e. there is an
> >underlying problem of "meaning" which, AFAIK, cannot really be
> >formalised (in this sense, any formalisation is a reduction to an
> >abstract game, just meaningless when taken on its own).
>
> It's true that there are problems with formalizing meaning. However, that
> isn't necessarily an obstacle to delegating the verification of proofs to
> a computer.
I still don't get how that could work *in general*, given not only
that meaning proper cannot be formalised, but also that even within
the realm of computation, it turns out not everything is actually
computable (or, at least, effectively computable).
-LV
Joshua Cranmer
> It is an objective fact that the XML people did not do a good
> job making it human readable. It is my personal opinion that
> they were not competent to do so.
I would consider it subjective--I think XML is rather human-readable.
The main problem that I think people have is that XML is designed to
delineate all structure, and people would rather that structure be inferred.
2 % 3 $ 4 would be an ambiguous, but
<expr operator="%">
<operand>2</operand>
<expr operator="$">
<operand>3</operand>
<operand>4</operand>
</expr>
</expr>
is not.
A lot is also dependent on the structure that people impose on XML
files. <e o="%"><o t="t">2</o><e o="$"><o t="t">3</o><o t="t">4</o></e>
is definitely harder to read.
One also needs to consider what exactly human-readable means. 99% or
more of XML will not be written by hand as they are merely storage
formats or transit formats. The primary case where they will be read by
humans is in debugging, or possibly some explanatory prose. In this, I
would say it is definitely human-readable (compared to binary protocols).
--
Beware of bugs in the above code; I have only proved it correct, not
tried it. -- Donald E. Knuth
Andrew Tomazos
> I still don't get how that could work *in general*, given not only
> that meaning proper cannot be formalised, but also that even within
> the realm of computation, it turns out not everything is actually
> computable (or, at least, effectively computable).
It's true that some things are not computable (halting), and also true
that some things cannot be proven (godel).
However our discussion is limited to verification of mathematical
proofs - so what is an example of a valid mathematical proof such that
its verification process is not computable?
I am not sure such a thing exists - almost by definition.
-Andrew.
tc...@lsa.umich.edu
The second concern first: not everything is effectively computable, yes.
However, what we're talking about here is verifying that an explicitly
exhibited proof is correct. The expectation of the mathematical community
is that when someone announces a proof and publishes it, everyone else (or
at least everyone who has sufficient training) can verify it. It is also
understood that even though every natural-language argument "skips" some
steps that are "obvious," it is possible in principle to flesh out those
details formally if necessary.
If these expectations are correct, then no uncomputability issues arise.
We're not talking about *finding* proofs, but *verifying a given proof*.
For a formal proof, that is certainly a finite computation.
Now, it is true that the process of fleshing out a "human" proof into a
*formal* proof is not a purely mechanical process, so this part cannot
be delegated to a computer. In practice, however, there have not been
any cases where human beings have agreed that a "human" proof is correct
but have run into fundamental obstacles converting it into a formal proof.
Something is still gained by introducing the computer, because the very
last part of the formalization can often be automated, and here the accuracy
of the computer comes into play.
The process is similar to programming an algorithm. I come up with an
algorithm for sorting. We argue about it using natural language and come
to a consensus that the algorithm is precisely specified and correct. Then
comes the implementation phase. The computer does not know what sorting
"means." It just crunches away. Nevertheless, in practice this does not
prevent us from implementing our sorting algorithms and agreeing that the
computer is running the algorithm. We also gain confidence that the
algorithm is correct after we've gone through the detailed process of
implementing it and trying it out.
tc...@lsa.umich.edu
Andrew Tomazos <and...@tomazos.com> wrote:
>We could in fact get there today, but all the systems (Mizar, HOL,
>Isabelle, etc) have had so little investment - and so few experienced
>developers work on them. Basically there isn't the impetus or money
>to make it happen quickly, probably because most mathematicians do not
>yet appreciate the potential benefit to their productivity.
I think you're too optimistic that we could "get there" *today*, if by
"getting there" you mean a benefit to *productivity*. We would get
increased confidence in the correctness of our published proofs, which
is a benefit to be sure, but I do not believe that incorrect proofs are
currently a bottleneck in mathematicians' *productivity*.
But we are getting close to the point where proofs are getting so large
that they are difficult to check. Sooner or later, "bugs" in the
mathematical literature *could* become a productivity killer. So it's
good to be proactive and start implementing a fix now before the problem
overtakes us.
tc...@lsa.umich.edu
Jan Burse <janb...@fastmail.fm> wrote:
>I can't believe the argument you are giving. It sounds like since
>formalized proofs are not readable now, we should not work in the
>direction of improving the readability. So you are making the alleged
>status quo as the future goal.
>
>First of all that formalized proofs are not readable, is this juts
>gut feeling of yours, or is this based on real experience?
Certainly, it is based on experience. Forget about computers even: A lot
of the time, I can't even understand a *human* proof when it is written too
formally. Usually I need the ideas to be explained informally before I can
understand what's going on. At that point, I often don't need to read the
proof because, understanding the idea, I can reconstruct the proof myself.
The argument I am making is not that formal languages should not be made
more readable. I am making the argument that formal proofs will never
supplant informal human communication as a vehicle for transmitting human
knowledge.
Now, let me argue on your behalf for a moment. I think that there could be
some room for building a layer *on top of* HOL Light or Mizar that more
closely mimics human proofs. At a sufficiently high level, after all, the
formal proof should be "the same" as a humanly understandable proof. The
analogy with computer programming would be a very high-level language in
which we can write the *specs* for a program. Then you could write software
that would translate such formal specs into, say, C++.
Following this analogy, what I am saying is that it is not a valid criticism
of C++ that it does not mimic human software specifications literally. That
is not the purpose of C++. Similarly, HOL Light is a high-level language,
but it is not *that* high, nor is it intended to be. It works at a much
lower level of detail. It is not a valid criticism of HOL Light that it
does not mimic human proofs literally.
Jan Burse
> How does this description of naming fit into the concerns you stated
> regarding objects that are conjectural in intuitionistic logic but
> proven in classical logic? This isn't clear to me.
> -Andrew.
Your publishing will be a stream with updates.
Andrew Tomazos
> > How does this description of naming fit into the concerns you stated
> > regarding objects that are conjectural in intuitionistic logic but
> > proven in classical logic? This isn't clear to me.
>
Ummm. What do you mean?
-Andrew.
Musatov
Dear Andrew:
I mean what you read. If you do not understand pick up a dictionary as
you read. Try to keep up. Marty
Tim Smith
<9e11ff68-c15b-4484...@o30g2000vbc.googlegroups.com>,
Andrew Tomazos <and...@tomazos.com> wrote:
> Furthermore, why isn't there a centralized proof web/database that
> contains all the axioms and verified proofs in some standard format?
> If we had some standard naming reservation system than you could use
> an old theorem from one verified proof in the database as a "basis
> axiom" for a new proof.
You might find <http://www.vdash.org/> interesting.
--
--Tim Smith
MeAmI.org
> In article
> <9e11ff68-c15b-4484-9582-b01adddb9...@o30g2000vbc.googlegroups.com>,
Dear USENET,
Below is NP=P machine checkable proof text. It points to M.I.T. as
part of the proof and it was generated by typing the words "NP=P
Complete Machine Checkable Proof" in the "pre-html" Custom Search at
http://MeAmI.org.
For Verification here is the link:
http://meami.org/?cx=000961116824240632825%3A5n3yth9xwbo&cof=FORID%3A10&ie=UTF-8&q=NP%3DP+Complete+Machine+Checkable+Proof&sa=Search#1271
And the text:
NP (complexity) - The existence of problems outside both P and NP-
complete in this case was established by Ladner. [....] A
nondeterministic machine can simply nondeterministically run the [...]
NP can be seen as a very simple type of interactive proof system,
[...] solvable by probabilistically checkable proofs where the
verifier uses [...]
http://en.wikipedia.org/wiki/NP_(complexity)
Complexity Zoo:P - Qwiki [...] The canonical P-complete problem is
circuit evaluation: given a [....] PCP(r(n),q(n)): Probabilistically
Checkable Proof [...] It was shown in [CPO7] that if the NP Machine
Hypothesis holds, then \mathsf{P}^{\mathrm{SAT}[1]} [...]
http://qwiki.stanford.edu/wiki/Complexity_Zoo:P
List of complexity classes - NE, Solvable by a non-deterministic
machine in exponential time with linear exponent [...] NP, "YES"
answers checkable in polynomial time (see complexity classes P and NP)
[...] Solvable in polynomial time. P-complete, The hardest problems in
P to solve on parallel computers [...] PCP, Probabilistically
Checkable Proof [...]
http://en.wikipedia.org/wiki/List_of_complexity_classes
School of Informatics Courses: Computer Science 4: Computational [...]
Proof that NP=P if and only if satisfying assignments can be found for
[...] Use of the technique to show there is an NP-complete problem in
non-deterministic linear time. [...] Definition of Randomized Turing
machine (RTM) and randomized time complexity [...] to theory of
probabilistically checkable proof (PCP) systems. [...]
http://www.inf.ed.ac.uk/teaching/courses/cmc/lecture_log.html
A Note on Non-complete Problems in NP[...]NP"P (in the classical
Turing machine setting) if P{NP is assumed. In [.....] So as in the
proof of Theorem 1 we can write and check (again by means [...]
http://linkinghub.elsevier.com/retrieve/pii/S0885064X9990537X
by S Ben-David - 2000 - Cited by 12 - Related articles - All 4
versions
Complexity classes with complete problems between P and NP-Cin order
to check that a gb'en string w is in L', the robust machine only needs
[.....] the difference between P and NP is the ability of the NP-
machines to manufacture [...] shown previously to be complete in ilk.
The details of the proof [...]
http://www.springerlink.com/index/p6562j95u353rl14.pdf
Complexity class - Computer Science Complexity class: A community-
built table of topics, including P, NP, and NP-complete [...] In
complexity theory, the notion of P-complete decision problems is
useful in [....] Turing machine with an oracle for some decision
problem in NP. [...] In computational complexity theory, a
probabilistically checkable proof (in [...]
http://computerscience.freebase.com/view/base/views/complexity_class
[PDF] 1 Overview 2 Summary of Contents machine complexity theory to
include various other computational models such as [...] deterministic
Turing machines and defines the basic complexity classes, including P,
NP, PSPACE [...] Cook's theorem that SAT is NP-complete is proven, and
reductions are [...] Given a short proof, is it possible to check
correctness in [...]
http://www.utdallas.edu/~dxd056000/cs6382/review.pdf
by DZ Du - 2003
\documentclass{article} \usepackage{amsmath} \input{preamble.tex [...]
\begin{section}{NP and P/poly }\end{section} For a sketch of the
proof, [...] $(s_1,[...],s_l)$, first check to make sure that $|s_i| <
(ki)^k$ for $1\leq i \leq l$. [....] we present a Turing machine that
decides the $\Sigma_3 P$-complete [...]
http://www-math.mit.edu/~spielman/AdvComplexity/2000/lecture5.tex
Np: Definition from Answers.com The existence of problems outside both
P and NP-complete in this case was established by Ladner. [....] A
nondeterministic machine can simply nondeterministically run the [...]
NP can be seen as a very simple type of interactive proof system,
[...] as the problems solvable by probabilistically checkable proofs
where the [...]
http://www.answers.com/topic/np
Andrew Tomazos
A formal mathematics wiki that only allows true statements. This is
an interesting idea. I have two comments:
1. As discussed, there are various different logics and hence what
is true in one is not necessarily true in another. How would vdash
handle this?
2. I'm not sure mathematicians will be prepared to just donate their
proofs anonymously and unattributed. Won't they want someway of
identifying and authenticating who proved what?
Idea: Maybe there could be a place for anyone to put conjecture
statements on the wiki, but the proofs of those conjectures must be
submitted by one author, and only accepted if true, and the author
would get credit and sole access to write some paragraph on the proof
page.
-Andrew.
Musatov
I tell you the truth, those who have earned will be recognized.
I will show you the way.
"3SAT is Not Too Easy."
A Future Retrospective In Computational Complexity
Read Gödel's Lost Letter and P=NP. Also check out Iannis Tourlakis'
paper on extensions of these lower bound. What I find nice about this
type of proof is you get lower bounds by finding new algorithms.
How to Solve P=NP? Gödel's Lost Letter and P=NP was a good start but
we all guessed wrong. Gödel's Lost Letter and P=NP led to a discussion
and proof that \mathsf{NLOG} is closed under complement. Perhaps we
should put P=NP on theory exams and hope \dots [...].
I am serious. All the properties are easy to check. The main point is
if the machine guesses wrong during the computational complexity
theory, P = NP if and only if there exists a Turing machine T and a
natural number k such that <j>(ri) < nk, the question already
considered by Godel!
Computational Complexity: Gödel Prize 12 Apr 2006 [...] Even proving
it couldn't be done would solve the P/NP puzzle. [...] NP because it
seems very counter intuitive to say that we can check an exponential
number of [...]. Obviously it's not a formal proof, but it is an
intuitive coding.
Imagine some time in the future the problem has been solved and we
have read an article including an interview with the ingenious
programmer who solved the P vs. NP problem. [Note: I only use the word
"ingenious" here as it is cited in the P vs. NP problem description:
http://www.claymath.org/millennium/P_vs_NP/ from the Clay Mathematics
Institute: (excerpt )"However, this apparent difficulty may only
reflect the lack of ingenuity of your programmer."]
Imagine the article interviewing the programmer contained:
"Well, I thought I may not be able to prove P = NP by traditional
means, but I can certainly prove NP ! [....]. Hey Atwood, here's a
suggestion for your next article on Godel's Theorem. [.....] And Jeff
cashes yet another nice check from the controversy his blog has [....]
proof, establishing that 3-SAT could be reduced to 2SAT in O(n3)
time."
What can I say? It is the Power of randomness: Efficient Computation &
P vs. NP.
Gödel's letter to von Neumann [1954]: [...] Probabilistically
Checkable Proofs (PCPs). Claim: The Riemann Hypothesis. Prover:
(argument)[...] Every proof can be efficiently transformed to ZK proof
[...].
An Argument for P=NP: the winner needn't provide a constructive proof
that P=NP. 2. Despite Godel's [...] Godel, writing of course before
the modern P=?NP framework, inquires [.....]. By definition, a guess
for an NP problem is checkable in polynomial time. [...]
Imagine possibilities, conceive, wonder, speculate, discover!
Complex Multi-Tiered Abstracts:
Abstract: It is shown how to restrict Gödel's system $T$ of recursion
in all higher [...] Abstract: We discuss the forcing approach to P==NP
problem. [...] sound" proof-systems) showed how to efficiently check
proofs of [...].
Then mathematics, science, technology, innovation, and most
importantly advances in medicine, (still governed by fundamental
physics--bases of reality) become more like storytelling.
"Imagination is more important than intelligence." --Albert Einstein
"The Tale of NP-Completeness"
By [...]
1931 – Kurt Gödel introduces the incompleteness theorems [...]. First
Formal Proof that P NP. By giving a poly-time solution for the
matching search problem, [....] find a proof then check it? - [YES].
Is nature non deterministic? [YES].
A Short History of A Short History of Computational Complexity
By Martin Musatov
It was a dark night in Los Angeles. I was curled up on a futon at a
friend's downtown loft (4th & Broadway), writing a USENET post at 4
AM. "Man, they are going to think you're obsessed." I thought as I
poked at the tiny QWERTY keyboard of my BlackBerry.
--
Martin Musatov
http://MeAmI.org
"Better than Google alone, plus no ads."
Jan Burse
> Irrelevant bla bla
fuck off
Jan Burse
This looks definively nice. To solve all the already mentioned
problems, like different styles, different logics, the wiki could
be self explaining. Right down to the primitives it uses in its
machinery.
Bye
tc...@lsa.umich.edu
Andrew Tomazos <and...@tomazos.com> wrote:
>On Jun 21, 5:36�am, Tim Smith <reply_in_gr...@mouse-potato.com> wrote:
>> You might find <http://www.vdash.org/> interesting.
Thanks for the pointer...I wasn't aware of this until now.
> 1. As discussed, there are various different logics and hence what
>is true in one is not necessarily true in another. How would vdash
>handle this?
It appears that the plan is to stick to classical logic. This is a
reasonable decision since the vast majority of existing mathematics is based
on classical logic.
> 2. I'm not sure mathematicians will be prepared to just donate their
>proofs anonymously and unattributed. Won't they want someway of
>identifying and authenticating who proved what?
This is an astute point which doesn't seem to be addressed directly in any
of the documentation. It seems like it shouldn't be too hard to add such a
feature, though.
Joshua Cranmer
> You might find <http://www.vdash.org/> interesting.
I've previously looked at Metamath, but this seems much more usable.
Herman Rubin
<tc...@lsa.umich.edu> wrote:
>In article <6fcb7f97-1d1a-4121...@l32g2000vba.googlegroups.com>,
>Andrew Tomazos <and...@tomazos.com> wrote:
>>> You might find <http://www.vdash.org/> interesting.
>Thanks for the pointer...I wasn't aware of this until now.
>> 1. As discussed, there are various different logics and hence what
>>is true in one is not necessarily true in another. How would vdash
>>handle this?
>It appears that the plan is to stick to classical logic. This is a
>reasonable decision since the vast majority of existing mathematics is based
>on classical logic.
>> 2. I'm not sure mathematicians will be prepared to just donate their
>>proofs anonymously and unattributed. Won't they want someway of
>>identifying and authenticating who proved what?
Why is it necessary that the proof be anonymous?
>This is an astute point which doesn't seem to be addressed directly in any
>of the documentation. It seems like it shouldn't be too hard to add such a
>feature, though.
>Tim Chow tchow-at-alum-dot-mit-dot-edu
--
This address is for information only. I do not claim that these views
are those of the Statistics Department or of Purdue University.
Herman Rubin, Department of Statistics, Purdue University
hru...@stat.purdue.edu Phone: (765)494-6054 FAX: (765)494-0558
Spiros Bousbouras
> On Jun 19, 2:22 am, Spiros Bousbouras <spi...@gmail.com> wrote:
>
> > Note that many computer programmes have silly bugs
> > which a human reader would immediately pick up but a compiler might
> > not. So it is possible that due to such a silly bug in the source
> > of a proof the computer will say that a proof is correct when
> > actually it is not.
>
> No, that's not what would happen. If the *proof verifier* is
> buggy, it might reject a correct proof or accept an incorrect
> proof. If the human is confused, he might decide that the
> proof said one thing when it really said a different thing.
>
> But the proof itself says what it says, and can't say anything
> different from that.
By the same reasoning a computer programme cannot have bugs because
it says what it says and the computer is just executing the
instructions.
--
Who's your mama?
Spiros Bousbouras
> In article <h1gj84$3...@odds.stat.purdue.edu>,
>
> Herman Rubin <hru...@odds.stat.purdue.edu> wrote:
> >While it is true that any theorem has a completely computer
> >verified formal proof, and possibly some should have a more
> >formal proof "published", as of yet it generally takes too
> >much work to even produce the formal proof.
>
> Too much work for the average mathematician, yes. But too much work for
> someone with an interest in the subject, no. See for example
>
> http://www.cs.ru.nl/~freek/100
>
> for a list of theorems that have been fully formalized.
I think Andrew's vision is that every mathematical proof will be
computer verified before being published in a journal. So it
shouldn't be too much work for the average researcher
mathematician.
Marshall
No, not at all.
A bug in a program is usually a difference between the
programmer's intent and what the programmer actually wrote.
This corresponds to the case I described above where
the human believes the proof means one thing but as
actually written it means something else.
Marshall
Spiros Bousbouras
> On Jun 19, 11:22 am, Spiros Bousbouras <spi...@gmail.com> wrote:
>
> > > If yes, is it also true that all of these deductions could be written
> > > in such a way that a computer program can infallibly verify the
> > > correctness of these steps?
>
> > If the verifier does not contain bugs and runs on top of an
> > operating system whose possible bugs will not adversely influence
> > the correct functioning of the verifier and both the verifier and
> > the operating system run on top of hardware whose possible bugs
> > will not adversely influence the correct functioning of the
> > verifier and the verifier receives correct input then the answer is
> > yes. There are several programmes which do this.
>
> Yes, but couldn't the language that the machine-readable proof is
> written in be specified as a standard. That way several
> implementations of verifiers could be developed for different hardware
> and operating systems (as is common for most heavily used programming
> languages).
Yes , that's a possibility. Of course someone needs to write the
standard and prove that it's correct meaning that an implementation
of the standard will say that a proof is true if and only if it is
true.
> It seems as though the basic rules of verifying FOL from an
> implementation point-of-view are quite trivial. ie There isn't a lot
> that could go wrong. In any case, surely we must agree that such a
> system would be significantly more reliable than what we do now.
Let's consider FOL in the language of ZFC where the vast majority
of mathematical theorems are written and proved. If the verifier
only accepts FOL and nothing else then every time your proof
contains for example something like x+y where x and y are real
numbers then you would need to rewrite it using only logical
symbols and epsilon. This would be a huge amount of work and
completely unworkable. So the verifier would also need to
understand not just the formal language of set theory but also all
the shorthands mathematicians use in their practice. But then it
must also have some kind of type system so that it can check that
when you write x+y the + part is meaningful for the kind of object
x and y are. But what if x and y are different kinds of objects ?
Say x is natural and y real. Your system probably also needs some
kind of types promotion so that x also gets treated as a real when
you write x+y. The language standard needs to specify how these
type promotions work.
I'm sure it's doable but it's quite more complicated than what you
make it out to be. It's not obvious to me that it would be
significantly more reliable than what we have now if at all.
Personally I'm very thorough when checking my proofs. Such a system
might help me do things quicker but it wouldn't improve my
reliability.
> > > If also yes, than why isn't it required that the centerpiece of any
> > > published proof be the "source code" for such a computer verification?
>
> > Because mathematics proofs have existed for a lot longer than
> > computers and there isn't a strong enough incentive to change
> > things.
>
> Well, the incentive is that we would have a near infallible and
> scientific way to verify any mathematical theorem - with an instant
> and impartial peer-review process. Surely it would save a lot of time
> in determining whether a proof is valid or not.
The "scientific" claim is vague. As for the rest I can only say
perhaps. More tests are needed.
> > > ie Shouldn't the center of every proof be a machine-readable theorem
> > > and machine-readable steps to undeniably deduce that theorem? The
> > > English should just be annotation essentially.
>
> > Why do you think it should ? It's not obvious that it will increase
> > correctness. Note that many computer programmes have silly bugs
> > which a human reader would immediately pick up but a compiler might
> > not. So it is possible that due to such a silly bug in the source
> > of a proof the computer will say that a proof is correct when
> > actually it is not.
>
> I don't see how it could not increase correctness? How could a machine-
> verified proof be incorrect? What is an example of a "silly bug" that
> might be in a theorem verifier? It seems like all the steps to verify
> a proof are very straightforward and simple. The steps seem ideally
> suited to machine.
The bug in the verifier could be the kind of bug which may exist in
any other piece of software. But I said "bug in the source of a proof"
meaning what you feed to the verifier even if the verifier itself
does not have bugs. I have been thinking about that and the most
dangerous possibilities I could think of are:
a) You give the verifier the wrong theorem to prove instead of what
you have in mind.
b) One of the intermediate lemmas you say to the verifier are
correct is not actually correct.
b) can be solved if the verifier verifies *everything*. Of course
that means someone actually needs to write down a formal proof for
every trivial little thing like for example that the union of
finite many finite sets is finite. a) doesn't seem particularly
dangerous.
Obviously just because a) and b) are the only possibilities I could
think of for bugs in the proof doesn't mean no other possibilities
exist. Once again more tests are needed.
> Very interesting. This "Mizar system" and the "QED project" are
> exactly what I am suggesting. My question is why haven't they evolved
> into the standard way of publishing proofs?
Presumably because most people are fairly satisfied with the way
things are now. I had looked into Mizar myself at some point.
Information was hard to come by. For example I was only able to
find a tutorial for an older version of the language. I didn't see
any formal specification. I think there's only one implementation
and it's closed source. If I am correct in all that then Mizar is a
no no as far as I'm concerned.
> > > If we had some standard naming reservation system than you could use
> > > an old theorem from one verified proof in the database as a "basis
> > > axiom" for a new proof.
>
> > > What am I missing?
>
> > One of the things I want to try out at some point is to write my
> > own proof verifier and see how it affects my productivity and
> > whether using it to verify proofs might introduce mistakes I wouldn't
> > otherwise make. So basically I believe more experimentation is
> > needed by as many mathematicians as possible before reaching
> > conclusions.
>
> I'm sure writing a machine-readable proof is more difficult than
> taking some steps for granted or based on intuition - but the
> advantage of the former is that it is virtually infallible.
Perhaps.
> Isn't
> that what mathematics is all about? Rigorous and undeniable steps
> from axioms to theorems?
I happen to agree with you on that but I may be in the minority.
I'm sure you would find many mathematicians who consider beauty
just as important and they won't think that typing a bunch of
tedious details for the benefit of a computer adds anything to the
beauty of the ideas behind the proof. If anything it detracts from
them. Apart from that noone wants to get bored out of their head.
--
This film, alas, is not "The Tempest," a self-referential perspective
on an artist who understands his own magic. It is instead an echo of
that artist's misunderstanding of himself.
http://www.imdb.com/title/tt0091670/usercomments?start=10
Spiros Bousbouras
It also corresponds to what I described when I said "the computer
Andrew Tomazos
> Again , what benefit to his productivity can a present day
> mathematician hope to gain if more investment was made on proof
> verifiers ?
Well if we assume that:
- we can design a formal proof language that is machine-readable
- the language is as human-readable as current natural language
proofs
- the length of a proof in that language is on-par with a natural
language proof
- the software gets good at finding truth-preserving pathways between
formulas
Then the software that a mathematician uses to write proofs would be
able to "follow along" with them, so you would get all of the benefits
that programmers get in their IDEs:
- auto-completion
- on-the-fly error checking
- top-down structure views
- dependency analysis
- hyperlinked definition lookup
- refactoring engine
- etc
Eventually, maybe, it would get to the stage where the software could
actually help find the proof itself. Wouldn't it be nice to state the
conjecture, and the computer goes off and writes the entire
proof? ...or at least fills in some of the non-obvious steps that
would *not* be omitted in a present day natural language proof?
A comment was made that computers are "superfast superimbeciles". I
am not so sure that is fair. Out of the factory with no software this
is the case. Getting away from that is a software problem. Search
algorithms and machine learning algorithms have come a long way. I am
not so sure that the full brunt of these algorithms have been applied
to the type of proof software under discussion.
-Andrew.
Spiros Bousbouras
> On Jun 22, 3:01 am, Spiros Bousbouras <spi...@gmail.com> wrote:
>
> > Again , what benefit to his productivity can a present day
> > mathematician hope to gain if more investment was made on proof
> > verifiers ?
>
> Well if we assume that:
> - we can design a formal proof language that is machine-readable
> - the language is as human-readable as current natural language
> proofs
> - the length of a proof in that language is on-par with a natural
> language proof
> - the software gets good at finding truth-preserving pathways between
> formulas
The first 2 tasks are fairly easy , they may even be already true.
The 3rd task may be impossible. I'm not sure what you mean with the
4th task.
> Then the software that a mathematician uses to write proofs would be
> able to "follow along" with them, so you would get all of the benefits
> that programmers get in their IDEs:
> - auto-completion
> - on-the-fly error checking
> - top-down structure views
> - dependency analysis
> - hyperlinked definition lookup
> - refactoring engine
> - etc
I don't know what "top-down structure views" is but the rest are
fairly trivial ; I don't think they would affect the speed of
typing proofs. Well , auto-completion might but you get that with
any decent text editor , it hasn't got much to do with proof
verification.
> Eventually, maybe, it would get to the stage where the software could
> actually help find the proof itself. Wouldn't it be nice to state the
> conjecture, and the computer goes off and writes the entire
> proof? ...or at least fills in some of the non-obvious steps that
> would *not* be omitted in a present day natural language proof?
It wouldn't be nice if it causes some mathematicians to lose their
jobs. But that's a completely different discussion.
Spiros Bousbouras
> On Jun 19, 11:30 am, Spiros Bousbouras <spi...@gmail.com> wrote:
>
> > On 19 June, 09:34, Andrew Tomazos <and...@tomazos.com> wrote:
>
> > > If yes, is it also true that all of these deductions could be written
> > > in such a way that a computer program can infallibly verify the
> > > correctness of these steps?
>
> > > published proof be the "source code" for such a computer verification?
>
> > <http://en.wikipedia.org/wiki/Kepler_Conjecture#A_formal_proof>
>
> Yes, but this is a proof by exhaustion. I'm asking why all kinds of
> proofs are not required to be machine verified?
I don't know what "proof by exhaustion" means. In any
case it's a complicated proof and if you're going to have
proof verification by computers you want it the most for
the most complicated proofs.
Andrew Tomazos
> > Then the software that a mathematician uses to write proofs would be
> > able to "follow along" with them, so you would get all of the benefits
> > that programmers get in their IDEs:
> > - auto-completion
> > - on-the-fly error checking
> > - top-down structure views
> > - dependency analysis
> > - hyperlinked definition lookup
> > - refactoring engine
> > - etc
>
> I don't know what "top-down structure views" is but the rest are
> fairly trivial ; I don't think they would affect the speed of
> typing proofs. Well , auto-completion might but you get that with
> any decent text editor , it hasn't got much to do with proof
> verification.
No, I don't just mean auto-completing and error-checking latex macros,
I am talking about larger logical sections of the proof. Entire
forumalas, or a entire sequence of deductions. It is my understanding
that some proofs take years to complete, so I'm not too sure how these
things can be "fairly trivial".
-Andrew.
Marshall
If the human operator chose a theorem that was other
than the one he meant to choose, and supplied the
verifier with a valid proof which the verifier accepted,
I would object to describing that situation as one in which
"the computer will say that a proof is correct when
actually it is not."
In that situation, the proof is indeed correct; it is just
that it is a proof of something other than the operator
thought it was.
Marshall
Andrew Tomazos
> I don't know what "proof by exhaustion" means.
MeAmI.org
MeAmI.org wrote:
Dear Andrew,
Proof by exhaustion means, for example, how Archimedes arrived at the
value for pi by simply tracing smaller and smaller polygons over the
area of a circle. He kept doing it until the number arrived.
--
musatov
support a cure to childhood cancer
http://alexslemonade.org
Spiros Bousbouras
As I pointed out in a previous post it seems to me that this
analysis can be applied just as well to a computer programme and be
used to conclude that every computer programme is correct.
If you're happy with such a conclusion fine , I'm not.
More to the point , my comments (and everyone else's) should be
interpreted while keeping in mind the central issue of the
discussion which is , IMO , reliability of mathematical proofs and
whether it can be improved by using computer verifiers. A situation
where a mathematician believes she has a proof of theorem XYZ ,
feeds a formal version of the proof to the verifier and walks away
thinking that the verifier found the proof correct when in reality
the verifier did not , is clearly a reliability issue. For an
appropriate definition of "correct" you could say that even in such
a case the verifier verified a correct proof and in a similar
manner you could say that every computer programme is correct but I
don't believe this is a notion of "correctness" anyone has any use
for nor do I feel it is relevant to this discussion.
Spiros Bousbouras
I've read the article and I'm not convinced "Proof by
exhaustion" is a meaningful term. You could pretty
much say that every proof is a proof by exhaustion.
The lack of references in the Wikipedia article suggests
to me that someone came up with the notion out of thin
air and decided to write a Wikipedia article.
William Hale
<fd96f48e-ba10-42ac...@z9g2000yqi.googlegroups.com>,
Spiros Bousbouras <spi...@gmail.com> wrote:
I think that there are at least two different meanings here.
One meaning is whether a computer program is syntactically correct and
has the necessary libraries included: that is, the computer program
compiles successfully. Of course, not all computer programs that are
written compile successfully.
I take computer verification of a mathematical proof to be similar to
this meaning of a compiler verifying that a computer program can be
compiled. The computer verification of a mathematical proof yields that
there is no invalid step or else list the invalid steps in the given
proof.
Another meaning is whether a computer program fulfills the given
specification. This is a much more difficult problem, and seems to be
closely related to doing a computer verified mathematical proof. I don't
think that we are close in achieving this for computer programs or for
mathematical proofs.
The second meaning depends upon doing the first meaning. Since the first
meaning has not been completely done (in fact, has only started being
done), I think it is worthwhile to indicate why that step is important,
even if we don't do the second step. In particular, even if the
implementation of the first step has bugs, it still can point out errors
in incorrect proofs. And, in those cases where it points out an error
that is not an error, then that problem can be fixed.
Andrew Tomazos
> On 23 June, 05:51, Andrew Tomazos <and...@tomazos.com> wrote:
>
> > On Jun 22, 5:08 am, Spiros Bousbouras <spi...@gmail.com> wrote:
>
> > > I don't know what "proof by exhaustion" means.
>
> >http://en.wikipedia.org/wiki/Proof_by_exhaustion
>
> I've read the article and I'm not convinced "Proof by
> exhaustion" is a meaningful term.
It's not rocket science. The computer-based proof of the "Four Color
Theorem" reduced the problem to about 2000 cases. They then used a
computer to exhaustively prove each of those 2000 cases. This is a
"Proof by Exhaustion", where a large number of cases are proved
individually. It is a type of proof that a computer is better suited
for than a human. I was just pointing out that we were not discussing
just these types of proofs, but all types.
-Andrew.
Marshall
Wonderful. We have come full circle and made no progress
whatsoever.
There are distinctions to be drawn between the two cases;
if you are happy ignoring the distinction, fine; I'm not.
> More to the point , my comments (and everyone else's) should be
> interpreted while keeping in mind the central issue of the
> discussion which is , IMO , reliability of mathematical proofs and
> whether it can be improved by using computer verifiers. A situation
> where a mathematician believes she has a proof of theorem XYZ ,
> feeds a formal version of the proof to the verifier and walks away
> thinking that the verifier found the proof correct when in reality
> the verifier did not , is clearly a reliability issue. For an
> appropriate definition of "correct" you could say that even in such
> a case the verifier verified a correct proof and in a similar
> manner you could say that every computer programme is correct but I
> don't believe this is a notion of "correctness" anyone has any use
> for nor do I feel it is relevant to this discussion.
The reliability issue you describe is real. It is also outside the
scope of what can be mechanized, hence it is irrelevant
to the discussion of mechanical verification. It is of course
relevant to the discussion of producing the software and/or
mathematics we want.
Marshall