4 ms·

A formally rigorous proof of this (in Metamath) is here: http://us.metamath.org/mpeuni/0.999....html http://us.metamath.org/mpeuni/0.999....html Unlike typica

A formally rigorous proof of this (in Metamath) is here: http://us.metamath.org/mpeuni/0.999....html 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.

317070 7y ago
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.
- _Donny 7y ago
  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
  - shawnz 7y ago
    That causes a contradiction which is why infinity can't be used that way. But what is the contradiction with 0.999... = 1?
    - jl2718 7y ago
      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.
  - alanbernstein 7y ago
    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.
    - klank 7y ago
      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).
- dwheeler 6y ago
  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 http://us.metamath.org/mpeuni/mmcomplex.html
Recursing 7y ago
Very cool page! The only interesting step is step 32, which is just an application of http://us.metamath.org/mpeuni/geoisum1c.html 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 http://us.metamath.org/mpeuni/geoisum1.html. They key steps for that are http://us.metamath.org/mpeuni/geolim2.html http://us.metamath.org/mpeuni/geolim2.html and http://us.metamath.org/mpeuni/isumclim.html http://us.metamath.org/mpeuni/isumclim.html , which is indeed the crux of the issue
null0pointer 7y ago
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.
dahart 7y ago
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.

317070 7y ago

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.

_Donny 7y ago
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
- shawnz 7y ago
  That causes a contradiction which is why infinity can't be used that way. But what is the contradiction with 0.999... = 1?
  - jl2718 7y ago
    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.
- alanbernstein 7y ago
  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.
  - klank 7y ago
    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).
dwheeler 6y ago
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 http://us.metamath.org/mpeuni/mmcomplex.html

Recursing 7y ago

Very cool page! The only interesting step is step 32, which is just an application of http://us.metamath.org/mpeuni/geoisum1c.html 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 http://us.metamath.org/mpeuni/geoisum1.html. They key steps for that are http://us.metamath.org/mpeuni/geolim2.html http://us.metamath.org/mpeuni/geolim2.html and http://us.metamath.org/mpeuni/isumclim.html http://us.metamath.org/mpeuni/isumclim.html , which is indeed the crux of the issue

null0pointer 7y ago

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.

dahart 7y ago

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.