7 ms·

> This proof showed that “1 + 1”, does indeed equal “2”. It took 2 volumes to get here. I know this seems logical to mathematicians, but it feels to me like ha

> This proof showed that “1 + 1”, does indeed equal “2”. It took 2 volumes to get here. I know this seems logical to mathematicians, but it feels to me like having to take 2 volumes to prove something than any child knows intuitively is... I don't know what word I am looking for... obsessive?

Twisol 6y ago
You can imagine "1 + 1 = 2" not as an important question in this context, but rather a proof of concept for the system they devised. It's a bit like the story about a "black triangle" [0]: a rather useless model passed through a rendering pipeline to produce a result any OpenGL novice can scramble in a couple dozen lines, but showing that the whole pipeline does, indeed, actually work as intended. [0] https://rampantgames.com/blog/?p=7745 https://rampantgames.com/blog/?p=7745
FrozenVoid 6y ago
The idea is that 1+1 proof is made without the mathematical apparatus(High-level language) available after 1+1, i.e. its like a huge Assembler bootloader made from verified primitives(logical primitives) to load an operating system with High-level API(Mathemathics).
leetcrew 6y ago
we mostly live our lives as if P!=NP, but that does not detract from the importance of proving it.
jandrese 6y ago
The point was to prove that math wasn't an arbitrary human construct, that it was rooted in the fundamental nature of reality.
dddbbb 6y ago
They didn't set out to explicitly prove 1+1=2, they just got around to it after 2 volumes, it didn't require 2 volumes of background. A direct proof of 1+1=2 is pretty short in most logical systems.
NoodleIncident 6y ago
They're describing a new "programming" language, and demonstrating their "hello world".
redvenom 6y ago
The point is not to prove that 1+1=2. The point is to construct mathematics (all of mathematics) directly from the axioms using a formal language. The objective of 1+1=2 is not interesting, but the result is a rigorous foundation of mathematics using formal languages. The upshot is twofold: (1) we have a rigorous foundation of mathematics in formal logic which CAN be used to prove nontrivial statements, as in the application of model theory to mathematics, and (2) we can now build proof assistants that allow us to use computers to better understand proofs. Both applications of formal reasoning are equally interesting and have wide ramifications in mathematics.
justincredible 6y ago
How do we know that 1+1=2 without a proof or circular reasoning? If you think intuition is a good metric of truth, you should look into quantum mechanics.

Twisol 6y ago

You can imagine "1 + 1 = 2" not as an important question in this context, but rather a proof of concept for the system they devised. It's a bit like the story about a "black triangle" [0]: a rather useless model passed through a rendering pipeline to produce a result any OpenGL novice can scramble in a couple dozen lines, but showing that the whole pipeline does, indeed, actually work as intended. [0] https://rampantgames.com/blog/?p=7745 https://rampantgames.com/blog/?p=7745

FrozenVoid 6y ago

The idea is that 1+1 proof is made without the mathematical apparatus(High-level language) available after 1+1, i.e. its like a huge Assembler bootloader made from verified primitives(logical primitives) to load an operating system with High-level API(Mathemathics).

leetcrew 6y ago

we mostly live our lives as if P!=NP, but that does not detract from the importance of proving it.

jandrese 6y ago

The point was to prove that math wasn't an arbitrary human construct, that it was rooted in the fundamental nature of reality.

dddbbb 6y ago

They didn't set out to explicitly prove 1+1=2, they just got around to it after 2 volumes, it didn't require 2 volumes of background. A direct proof of 1+1=2 is pretty short in most logical systems.

NoodleIncident 6y ago

They're describing a new "programming" language, and demonstrating their "hello world".

redvenom 6y ago

The point is not to prove that 1+1=2. The point is to construct mathematics (all of mathematics) directly from the axioms using a formal language. The objective of 1+1=2 is not interesting, but the result is a rigorous foundation of mathematics using formal languages. The upshot is twofold: (1) we have a rigorous foundation of mathematics in formal logic which CAN be used to prove nontrivial statements, as in the application of model theory to mathematics, and (2) we can now build proof assistants that allow us to use computers to better understand proofs. Both applications of formal reasoning are equally interesting and have wide ramifications in mathematics.

justincredible 6y ago

How do we know that 1+1=2 without a proof or circular reasoning? If you think intuition is a good metric of truth, you should look into quantum mechanics.