Hacker News Reader

Comment by dwheeler | Hacker News Reader

A formally rigorous proof of this (in Metamath) is here:

http://us.metamath.org/mpeuni/0.999....html

Unlike typical math proofs, which hint at the underlying steps, every step in this proof only uses precisely an axiom or previously-proven theorem, and you can click on the step to see it. The same is true for all the other theorems. In the end it only depends on predicate logic and ZFC set theory. All the proofs have been verified by 5 different verifiers, written by 5 different people in 5 different programming languages.

You can't make people believe, but you can provide very strong evidence.

View on HN

It depends on more than just ZFC, also on the definitions of the real/complex numbers. The crux of the proof is that 0.99999... is being constructed within the real/complex numbers, and in that system it is equal to 1.

And at the point where students see this, the whole concept of real numbers and infinity is usually ill-defined. I actually understand the scepsis for this theorem and where it comes from. The proof relies on the existence of a supremum, which is non-trivial.

I think this is spot on, at least for me personally.

I am not very good at mathematics, so I never questioned my professors when they said that "You cannot treat infinites as regular numbers".

Perhaps due to that statement, I did not really pursue these kinds of equations. For instance, I do not really see how the algebraic argument on the Wiki is any different from:

  2 * inf = inf
  inf + inf = inf   (subtract inf from both sides)
  inf = 0

That causes a contradiction which is why infinity can't be used that way. But what is the contradiction with 0.999... = 1?

Multiply both sides by ‘x’, then subtract one side from the other, then take the limit as x -> inf. This is obviously undefined. To get to zero, you have to make a new rule that one form of infinity is bigger than another form of infinity.

Infinity is very slippery, and there are several divergent fields of math that depend on particular definitions of it.

There is this phrase, often used when describing the decimal expansion of pi - "keeps going infinitely". This phrase is not exactly incorrect, but I wonder if it misleads people into thinking that an "infinite decimal" is "a kind of infinity", which it really isn't in any meaningful way.

I think it absolutely gets confused.

Infinity, the number, is routinely confused with creating an onto function mapping digits of pi to a set with a cardinality of the natural numbers. But sadly most people don't have the mathematical maturity to understand the difference when they encounter their first irrational number (normally pi).

It's true that it depends on the definitions of real/complex numbers. Many other things turn out to be provable from ZFC. A discussion about this, from the viewpoint of Metamath, is here: http://us.metamath.org/mpeuni/mmcomplex.html

Very cool page!

The only interesting step is step 32, which is just an application of http://us.metamath.org/mpeuni/geoisum1c.html, whose only interesting step is step 21 which is just an application of http://us.metamath.org/mpeuni/geoisum1.html.

They key steps for that are http://us.metamath.org/mpeuni/geolim2.html and http://us.metamath.org/mpeuni/isumclim.html , which is indeed the crux of the issue

I wonder if this particular example does the opposite. It's too rigorous for a normal human. It seems humorously rigorous to state things like 10 is not equal to 0, and 10 is a real number and 1 is less than 10, not to mention the number of seemingly redundant repetitions showing how each of the numbers discussed is a complex number, separately an individually. Does defining 1+9=10 make the proof more believable?

Rigorous proofs like this are for mathematicians and computers, I doubt they help anyone believe who doesn't believe.

I'm not sure how best to help someone who doesn't believe, but it could take arguments with stronger intuition, or just allowing the person to demonstrate with their own proof. It probably depends on the person, and why they don't believe it.

That is cool! I've been thinking about building a site that lets you explore a big graph of math proofs for a long time, since doing my pure math degree. Glad to see someone else has done something like it.

Reply on news.ycombinator.com