 |
|
| Science Forum Index » Logic Forum » Computer-verified Mathematical Proof as Standard... |
|
Page 6 of 6 Goto page Previous 1, 2, 3, 4, 5, 6 |
|
| Author |
Message |
| ... |
 Posted: Wed Jun 24, 2009 7:59 am |
|
|
|
Guest
|
In article <aeb3fb95-a0d0-417a-9b4e-8224101bf935 at (no spam) l32g2000vba.googlegroups.com>,
Michel Hack <hack at (no spam) watson.ibm.com> wrote:
[quote:9a7759a97e]Translating a traditional math proof to a formal proof often involves
an exponential explosion in size, and sometimes MUCH worse (Ackermann-
like).
[/quote:9a7759a97e]
Do you have an example of a proof that has Ackermann-like explosion?
I'm not aware of one.
[quote:9a7759a97e]Now, perhaps there are automatic verifiers that can handle
transformations whose validity has been proved separately
-- but was THAT proof formal?
[/quote:9a7759a97e]
Yes, certainly. Any decent proof assistant has such capacities to one degree
or another. One motivation for the higher-order-logic based languages is
their ability to capture such "abbreviations" formally in a nice way.
--
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 |
|
|
| Back to top |
|
|
|
| Herman Rubin... |
| Posted: Wed Jun 24, 2009 12:13 pm |
|
|
|
Guest
|
In article <4a423140$0$515$b45e6eb0 at (no spam) senator-bedfellow.mit.edu>,
<tchow at (no spam) lsa.umich.edu> wrote:
[quote:8247f65077]In article <aeb3fb95-a0d0-417a-9b4e-8224101bf935 at (no spam) l32g2000vba.googlegroups.com>,
Michel Hack <hack at (no spam) watson.ibm.com> wrote:
Translating a traditional math proof to a formal proof often involves
an exponential explosion in size, and sometimes MUCH worse (Ackermann-
like).
Do you have an example of a proof that has Ackermann-like explosion?
I'm not aware of one.
[/quote:8247f65077]
No, but there are many proofs where one says, "in a
similar manner." These grow.
[quote:8247f65077]Now, perhaps there are automatic verifiers that can handle
transformations whose validity has been proved separately
-- but was THAT proof formal?
Yes, certainly. Any decent proof assistant has such capacities to one degree
or another. One motivation for the higher-order-logic based languages is
their ability to capture such "abbreviations" formally in a nice way.
[/quote:8247f65077]
I agree. This is not that difficult; a formal proof can
quote a theorem, but of course if the quote is of something
incorrect, the proof will not be valid. We do not have to
reinvent the wheel.
--
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
hrubin at (no spam) stat.purdue.edu Phone: (765)494-6054 FAX: (765)494-0558 |
|
|
| Back to top |
|
|
|
| ... |
| Posted: Wed Jun 24, 2009 6:44 pm |
|
|
|
Guest
|
In article <h1tqcl$433i at (no spam) odds.stat.purdue.edu>,
Herman Rubin <hrubin at (no spam) odds.stat.purdue.edu> wrote:
[quote:8afc0cf542]In article <4a423140$0$515$b45e6eb0 at (no spam) senator-bedfellow.mit.edu>,
tchow at (no spam) lsa.umich.edu> wrote:
Do you have an example of a proof that has Ackermann-like explosion?
I'm not aware of one.
No, but there are many proofs where one says, "in a
similar manner." These grow.
[/quote:8afc0cf542]
But they don't grow at a speed that defies formalization, which was the
topic of discussion.
The sort of thing that would (probably) be infeasible to formalize would
be a proof or disproof of "sin(2^2^2^2^2^2^2^2) > 0" (to borrow an example
of Harvey Friedman's). But we can't figure out whether that statement is
true or false informally either.
There could also be cases where a large cardinal axiom A allows you to
shorten the proof of a theorem T dramatically (though I don't think any
such case has arisen in "real life"). The you might have to settle for
formalizing the proof of the implication "A implies T" rather than
formalizing the A-free proof of T directly.
--
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 |
|
|
| Back to top |
|
|
|
| Aatu Koskensilta... |
| Posted: Thu Jun 25, 2009 5:47 am |
|
|
|
Guest
|
hrubin at (no spam) odds.stat.purdue.edu (Herman Rubin) writes:
[quote:c339c11d9c]In article <4a423140$0$515$b45e6eb0 at (no spam) senator-bedfellow.mit.edu>,
tchow at (no spam) lsa.umich.edu> wrote:
Do you have an example of a proof that has Ackermann-like explosion?
I'm not aware of one.
No, but there are many proofs where one says, "in a similar manner."
These grow.
[/quote:c339c11d9c]
But not in an "Ackermann-like" way.
--
Aatu Koskensilta (aatu.koskensilta at (no spam) uta.fi)
"Wovon man nicht sprechen kann, darüber muss man schweigen"
- Ludwig Wittgenstein, Tractatus Logico-Philosophicus |
|
|
| Back to top |
|
|
|
| Aatu Koskensilta... |
| Posted: Thu Jun 25, 2009 5:59 am |
|
|
|
Guest
|
tchow at (no spam) lsa.umich.edu writes:
[quote:564eec7023]There could also be cases where a large cardinal axiom A allows you to
shorten the proof of a theorem T dramatically (though I don't think any
such case has arisen in "real life").
[/quote:564eec7023]
There are no such cases.
--
Aatu Koskensilta (aatu.koskensilta at (no spam) uta.fi)
"Wovon man nicht sprechen kann, darüber muss man schweigen"
- Ludwig Wittgenstein, Tractatus Logico-Philosophicus |
|
|
| Back to top |
|
|
|
| Robert E. Beaudoin... |
| Posted: Thu Jun 25, 2009 7:41 pm |
|
|
|
Guest
|
Aatu Koskensilta wrote:
[quote:f764443eb7]tchow at (no spam) lsa.umich.edu writes:
There could also be cases where a large cardinal axiom A allows you to
shorten the proof of a theorem T dramatically (though I don't think any
such case has arisen in "real life").
There are no such cases.
[/quote:f764443eb7]
OK, I'll bite: What makes you so sure? I'm guessing you have some kind
of argument in mind; could you please share it?
Robert E. Beaudoin |
|
|
| Back to top |
|
|
|
| ... |
| Posted: Fri Jun 26, 2009 9:55 am |
|
|
|
Guest
|
In article <82eit8y14y.fsf at (no spam) A166.veli3.tontut.fi>,
Aatu Koskensilta <aatu.koskensilta at (no spam) uta.fi> wrote:
[quote:e529868862]tchow at (no spam) lsa.umich.edu writes:
There could also be cases where a large cardinal axiom A allows you to
shorten the proof of a theorem T dramatically (though I don't think any
such case has arisen in "real life").
There are no such cases.
[/quote:e529868862]
Meaning, I suppose, that the only candidates for T are artificial examples
such as "There is no ZFC-proof of 0=1 using less than 2^2^2^2^2^2^2^2
symbols."
--
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 |
|
|
| Back to top |
|
|
|
| Aatu Koskensilta... |
| Posted: Sat Jun 27, 2009 3:54 am |
|
|
|
Guest
|
tchow at (no spam) lsa.umich.edu writes:
[quote:f0407e39e8]Meaning, I suppose, that the only candidates for T are artificial
examples such as "There is no ZFC-proof of 0=1 using less than
2^2^2^2^2^2^2^2 symbols."
[/quote:f0407e39e8]
Yes. Or in other words, the possibility, while real, is currently
entirely theoretical. It would be very exciting to see this changed!
--
Aatu Koskensilta (aatu.koskensilta at (no spam) uta.fi)
"Wovon mann nicht sprechen kann, darüber muss man schweigen"
- Ludwig Wittgenstein, Tractatus Logico-Philosophicus |
|
|
| Back to top |
|
|
|
| MeAmI.org... |
| Posted: Thu Jul 02, 2009 3:36 pm |
|
|
|
Guest
|
[ABOVE IS MARTIN MICHAEL MUSATOV'S P==NP PROOF TEXT POSED AS A ...
{{x}}  L halts in Polynomial time.Let y  halts
in . ...http://www.docendi.org/re-t243853.html - 44k
Michael Press wrote:
[quote:6ce366383f]In article
aeb88920-8ae5-4858-b403-4483493f0908 at (no spam) k20g2000vbp.googlegroups.com>,
Andrew Tomazos <andrew at (no spam) tomazos.com> wrote:
On Jun 19, 7:02Â pm, Patricia Shanahan <p... at (no spam) acm.org> wrote:
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.)
I agree with the sentiment, but not the injunction.
Programmers will use anything, not dismiss anything
out of hand, and synthesize from everything they know.
I am a magpie, a picker up of unconsidered trifles.
--
Michael Press
If you meet the Buddha on the road, kill him.[/quote:6ce366383f] |
|
|
| Back to top |
|
|
|
| Michael Press... |
| Posted: Thu Jul 02, 2009 5:32 pm |
|
|
|
Guest
|
In article
<aeb88920-8ae5-4858-b403-4483493f0908 at (no spam) k20g2000vbp.googlegroups.com>,
Andrew Tomazos <andrew at (no spam) tomazos.com> wrote:
[quote:396939a0d0]On Jun 19, 7:02Â pm, Patricia Shanahan <p... at (no spam) acm.org> wrote:
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.)
[/quote:396939a0d0]
I agree with the sentiment, but not the injunction.
Programmers will use anything, not dismiss anything
out of hand, and synthesize from everything they know.
I am a magpie, a picker up of unconsidered trifles.
--
Michael Press
If you meet the Buddha on the road, kill him. |
|
|
| Back to top |
|
|
|
| Jimmy Niznick... |
| Posted: Sat Aug 08, 2009 11:55 pm |
|
|
|
Guest
|
Joshua Cranmer wrote:
[quote:f77e053537]Marshall wrote:
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
4. P=NP Proof Published at CERN (Musatov)[...]"standard practice when ... ever since 1971, extensive and <. .... published proof be the "source code" for ... </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).
Forgive Knuth, time to move on.[/quote:f77e053537]
+ MMM +
(Musatov) |
|
|
| Back to top |
|
|
|
| MichaelHH... |
| Posted: Sun Aug 09, 2009 12:36 pm |
|
|
|
Guest
|
Sir in Google groups you have changed the topic, this is unfair as
this thread has some interesting discourse. Please take your attitude
elsewhere.
If he bothers you this much get a reader and killfile him |
|
|
| Back to top |
|
|
|
|
|
All times are GMT - 5 Hours
The time now is Fri Dec 11, 2009 7:18 am
|
|