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 ]
 Jan Burse Posts: 1,472 Registered: 4/12/05
Re: Formal Proof Language Example - Human-Readable?
Posted: Jun 27, 2009 9:10 PM

Andrew Tomazos schrieb:
>>> In this step you have used:
>>> b = n*q*m
>>> c+a = q*n*n
>>> c-a = q*m*m

> We can assume that theorems about the nature of integer factorization
> have previously been established - but which ones specifically would
> we use to prove your above statements?

BTW: There is a nice motivation from computing
square roots for finding m and n:

Euler asks the question what could be
the value of sqrt(1+x^2)?

He sees that it is closed to x, and thus
he assumes

sqrt(1+x^2) = x + r

r = m / n

Now we have:

1 + x^2 = x^2 + 2*r*x + r^2

Hence:

2*r*x = 1 - r^2

Hence

x = (1 - r^2) / 2*r

Hence:

x = (n^2 - m^2) / 2*m*n

http://imgbase-scd-ulp.u-strasbg.fr/displayimage.php?album=381&pos=55

From this he then arrives at (n^2 + m^2)^2 = (n^2-m^2)^2+(2*m*n)^2.

But he doesn't ask whether this is a complete method for
the enumeration of all pythagorean triples.

Bye

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