If mathematical proofs were "nothing but a manner of convincing someone", how could it be verifiable by a computer?
Fully formal mathematical proofs depend on nothing but ability to distinguish characters, to compare text strings, and to perform substring substitution.
To your example (2 + 2 = 4). In formal arithmetics, based on Peano axioms, there is one primary operator, let's call it s:N -> N, and s(n) is interpreted as (n + 1). "2" is _defined_ as s(1). 3 is defined as s(2), and 4 is defined as s(3). So one has to prove that s(1) + s(1) = s(s(s(1))).
By definition of addition (remember, addition is not fundamental notion in the formal arithmetics, it's defined in terms of s-operator), a + s(b) = s(a + b), and a + 1 = s(a), so we have
s(s(1) + 1) = s(s(s(1))), s(s(s(1))) = s(s(s(1)))
Q.E.D.
So, where proof above depends on anything but mechanically verifiable string manipulations?
P.S., of course mathematical formulae are not strings, but rather trees, but this doesn't change a bit.
Slashdot Mirror
And this comment wasn't even written by Hans in the first place: http://nikitadanilov.blogspot.com/2007/06/and-now- to-subject-of-death.html
If mathematical proofs were "nothing but a manner of convincing someone", how could it be verifiable by a computer?
Fully formal mathematical proofs depend on nothing but ability to distinguish characters, to compare text strings, and to perform substring substitution.
To your example (2 + 2 = 4). In formal arithmetics, based on Peano axioms, there is one primary operator, let's call it s:N -> N, and s(n) is interpreted as (n + 1). "2" is _defined_ as s(1). 3 is defined as s(2), and 4 is defined as s(3). So one has to prove that s(1) + s(1) = s(s(s(1))).
By definition of addition (remember, addition is not fundamental notion in the formal arithmetics, it's defined in terms of s-operator), a + s(b) = s(a + b), and a + 1 = s(a), so we have
s(s(1) + 1) = s(s(s(1))),
s(s(s(1))) = s(s(s(1)))
Q.E.D.
So, where proof above depends on anything but mechanically verifiable string manipulations?
P.S., of course mathematical formulae are not strings, but rather trees, but this doesn't change a bit.
I should probably add that I am getting quite different bonnie++ results for reiser4 vs. ext3.
0 03.09.30
They are available at reiser4 benchmarking page along with
hardware specifications.
http://www.namesys.com/benchmarks.html#bonnie++.2