Search All of the Math Forum:

Views expressed in these public forums are not endorsed by NCTM or The Math Forum.

Notice: We are no longer accepting new posts, but the forums will continue to be readable.

Topic: Formal Proof Language Example - Human-Readable?
Replies: 39   Last Post: Jun 27, 2009 11:09 PM

 Messages: [ Previous | Next ]
 MeAmI.org Posts: 405 Registered: 6/14/09
Re: Formal Proof Language Example - Human-Readable?
Posted: Jun 22, 2009 4:01 AM

William Elliot wrote:
> On Sun, 21 Jun 2009, Andrew Tomazos wrote:
>

> > Please consider the following formal proof language example:
> >

> It's a pain in the butt to read.
> Here's the same which is much easier to read.
>
> Let N be the natural numbers.
> Proposition. For all a,b,c in N
> if a is odd, a,b are relative prime and
> a^2 + b^2 = c^2,
> then there's some m,n in N for which m <= n,
> a = n^2 - m^2,
> b = 2mn,
> c = n^2 + m^2.
> Proof. ...
>

> > package MyTheoryProof;
> > using edu.mit.number_theory.*;
> >
> > theorem MyTheory
> > {
> > let N be NaturalNumbers;
> > forall a, b, c in N
> > given
> > {
> > a^2 + b^2 = c^2;
> > a, b are_relative_prime;
> > a is odd;
> > }
> > implies
> > {
> > m <= n;
> > a = n^2 - m^2;
> > b = 2 * m * n;
> > c = n^2 + m^2;
> > }
> > }
> > proven_by
> > {
> > ...
> > }
> >
> > This is written in a Mizar-like language with some formatting changes
> > based on the C family tree and some personal touches.
> >
> > Without any description of the language, I'm curious to know whether
> > you can derive the meaning of the theorem statement simply by reading
> > the code? The goal is for it to be both machine and human readable.
> >
> > Thanks,
> > Andrew.
> >
> > --
> > Andrew Tomazos <andrew@tomazos.com> <http://www.tomazos.com>
> >

Musatov "null zero error!" sets dimensional time block, to [...]19 Jun
2009 [...] following his formal proof. [....] You see it is not my
intent with this writing to prove to you P=NP, I [....] Ivashev-
msg/a1e14406a0e976e4 - Discussions - comp.theory | Google Groups
Please consider the following formal proof language example: package
MyTheoryProof; [...] How to Solve P=NP? Gödel's Lost Letter and P=NP
was a good start but[...] more » [...] By Musatov - Jun 20 - 4 new of
Proof Published at CERN On 9 mayo, 05:18, Martin Musatov <marty.musa
[...]@xxxxxxxxx> wrote: An informal and highly experimental,
unorthodox proof P=NP has been [...]http://sci.tech-archive.net/
Archive/sci.math/2009-05/msg00792.html - The Awakening of The American
Mind: P=NP Incomplete___The Maximal [...]2) A complete and consistent
formal statement of the question must incorporate a [....]. So indeed
Mr. Musatov (triadic 3rd POV): has proven P=NP against the problem
[...] all still required is established for this "Musatov's proof
P=NP"[...]http://theawakeningoftheamericamind.blogspot.com/2009/03/pnp-
incompletethe-maximal-triadic.html P=NP Proof Published at CERN[...]
Martin Musatov wrote: Quote: An informal and highly experimental,
unorthodox proof P=NP has been published on CERN preprints. [...]
Published at CERN[...]adminship and bot requests may be less formal
and often go for a [......] [ABOVE IS MARTIN MICHAEL MUSATOV'S P==NP
PROOF TEXT POSED AS A [...]http://www.groupsrv.com/science/
about409940-0-asc-105.html [AvC] Re: P=NP iff N=NP Musatov said "P=NP
iff N=NP". "Iff" is short for "if and only if" [...] A fully formal
proof can certainly be checked in polynomial time, so the problem of
[...]http://www.mail-archive.com/atheism-vs-christianity
%40googlegroups.com/msg100421.html Math Forum Discussions 21 Jun 2009
[...] Formal Proof that P ? NP. By giving a poly-time solution for the
[...] By Martin Musatov It was a dark night in Los Angeles. [...]
1. The Chapter 2: God Math (Logik, LOGOS, P=NP) « Robot Pirate Ninja
This is my P=NP proof, after all. One would have to be a bit outside
the norm to put [....] as my formal education neared an end, the
answer came to me. [.....] EZZ = Musatov Proof: The Classes P and NP.
We now shift gears slightly and move [...]http://robotpirateninja.com/
1-the-chapter-2-god-math-logik-logos-pnp/ 11011110: Complexity
theoretologism Martin Musatov, a horror-film screenwriter, P=NP crank,
[...] The correct response, therefore, does not seem to me to be a
formal retraction or University [...] be for you to publish your P=NP
proof in a mathematics journal of international [...]http://
11011110.livejournal.com/168792.html

Date Subject Author
6/21/09 Andrew Tomazos
6/21/09 Jan Burse
6/21/09 Andrew Tomazos
6/21/09 Jan Burse
6/21/09 Andrew Tomazos
6/21/09 Jan Burse
6/21/09 Jan Burse
6/21/09 Jan Burse
6/21/09 Andrew Tomazos
6/21/09 Jan Burse
6/21/09 Andrew Tomazos
6/21/09 Jan Burse
6/21/09 Jan Burse
6/24/09 Andrew Tomazos
6/25/09 MeAmI.org
6/25/09 Jan Burse
6/26/09 Andrew Tomazos
6/27/09 Jan Burse
6/27/09 Andrew Tomazos
6/27/09 Jan Burse
6/27/09 Andrew Tomazos
6/27/09 Joshua Cranmer
6/27/09 Andrew Tomazos
6/21/09 Marshall
6/21/09 Spiros Bousbouras
6/24/09 Tim Smith
6/21/09 Charlie-Boo
6/21/09 William Elliot
6/22/09 MeAmI.org
6/22/09 MeAmI.org
6/23/09 Slawomir
6/24/09 David Bernier
6/24/09 MeAmI.org
6/24/09 MeAmI.org
6/24/09 Andrew Tomazos
6/24/09 Andrew Tomazos
6/25/09 Slawomir