# Metamath

Metamath is a project to construct mathematics as proofs in ZFC. This what what we’re all supposed to be doing but in practice proofs tend to be informal arguments that we can convince people could be converted into derivations in ZFC. It looks like a long haul. There are now over 5000 theorems proved but they’ve only just proved a<=b => a<=b+1 in the reals. On the other hand they seem to have several hundred proofs about Hilbert spaces and quantum logic. Meanwhile, Wim Hesselink is hoping to verify a proof of Fermat’s Last Theorem by machine.

## 9 thoughts on “Metamath”

1. PeterMcB on said:

Hesselink’s Fermat page mentions this prooblem as a challenge in theoretical computer science, part of a set recently articulated by Prof. dr. Jan Bergstra. As a computer scientist, I was interested to see this list of challenges, but had no success finding it. Do you happen to know if Bergstra’s Problems exist anywhere on the wetb?

2. sigfpe on said:

Here you go. Page 53. But there’s a slight catch…

3. PeterMcB on said:

Thanks. Problem 2 (a computer to play GO) is definitely a major problem, but the others are not IMHO. Perhaps I should have expected a *theoretical* computer scientist to ignore what I think are the major challenges in the discipline (modulo my Dutch translation).

4. knuddavid on said:

Would it not be easier to find a simpler proof of Fermat’s Last Theorem, formalize that, and verify that by computer?

I don’t pretend to have a proof but I suggest a different approach that Fermat himself (not having an electronic computer) might have tried.

The problem:

(1) a^n + b^n = c^n

This equation has integer solutions if â€˜n = 1â€™, or â€˜n = 2â€™; but not for any other integer value of â€˜nâ€™. It is evidently false for â€˜n = 0â€™, trivially true for â€˜n = 1â€™, and known to have solutions for â€˜n = 2â€™.
How would he go about proving it to be false for any higher number of â€˜nâ€™, given the constraint that only integer arithmetic was allowed?

The expression arose from a problem in geometry, and it is my guess that Fermat turned to the study of triangles for proof.

Stipulation:

(2) 0 2, for a solution to satisfy Eq.(1):

(5) c^n = (a^2 +b^2 – 2abcosC)^(n/2) = a^n + b^n + Rn

Excluding the special case: cosC = 0; with a,b,c being Pythagorean triples, if cosC (a^n +b^n ) for all values n > 2, (i.e. Rn > 0).

When cosC moves into positive territory, the andscape changes.
We have to rephrase Stipulation(2) to ensure that c remains the largest side of the triangle.

Since

(6) a = bcosC + ccosB

a sufficient condition for the current discussion is

(7) a > (b + c) cosC.

As cosC increases in value, the process ends in the frozen stalemate of the isosceles triangle, when

cosC = 0.5, and a = b = c.

We then have c^n

5. knuddavid on said:

I am new to this procedure, and shall continue where I was interrupted:

As cosC increases in value, the process ends in the frozen stalemate of the isosceles triangle,
when cosC = 0.5, and a = b = c.

We then have c^n

6. knuddavid on said:

Well, I try again. I hope the editor can splice it together:

As cosC increases in value, the process ends in the frozen stalemate of the isosceles triangle,
when cosC = 0.5, and a = b = c.

We then have c^n

7. knuddavid on said:

Once more, before I give up:

We then have c^n

8. knuddavid on said:

Sorry, this is not my day. In plain text:

Rn is zero only in the interval of cosC between 0 and 0.5.

In Eq.(3), if c is integer, its square must be integer, and the polynomial must be in quadratic form. This requires cosC = +/-1 in violation of the conditions for a solution of Eq.(1).

(I hope it works this time)

9. knuddavid on said:

Bear with me, I am thoroughly embarrassed. I believe my problems stem from the fact that I tried to copy a MSWord document, and the control characters are getting in the way.
I have now copied it in HTML format and done my best to edit the result:

Would it not be easier to find a simpler proof of Fermatâ€™s Last Theorem, formalize that, and verify that by computer?

The problem:
(1) a^n + b^n = c^n
This equation has integer solutions if â€˜n = 1â€™, or â€˜n = 2â€™; but not for any other integer value of â€˜nâ€™. It is evidently false for â€˜n = 0â€™, trivially true for â€˜n = 1â€™, and known to have solutions for â€˜n = 2â€™. How would he go about proving it to be false for any higher number of â€˜nâ€™, given the constraint that only integer arithmetic was allowed?
The expression arose from a problem in geometry, and it is my guess that Fermat turned to the study of triangles for proof.
Stipulation:

(5) c^n = (a^2 +b^2 – 2abcosC )n/2 = a^n + b^n + Rn

Excluding the special case: cosC = 0; with a,b,c being Pythagorean triples, if

cosC (a^n +b^n ) for all values n 0).

When cosC moves into positive territory, the landscape changes. We have to rephrase Stipulation(2) to ensure that c remains the largest side of the triangle. Since

(6) a = bcosC + ccosB

a necessary condition for the current discussion is

(7) a > (b + c) cosC.

As cosC increases in value, the process ends in the frozen stalemate of the isosceles triangle, when cosC = 0.5, and a = b = c. We then have c^n