3 ms·

> Is there a structure to mathematics which is independent of the human brain? I would venture to say "no". I don't think humans will ever have no place in mat

> Is there a structure to mathematics which is independent of the human brain? I would venture to say "no". I don't think humans will ever have no place in mathematics, because the problems we deem "important" are often relatively arbitrary. If a "post-human mathematician" starts spewing out thousands of pages of mathematics a second, all in a form only a computer can understand, no one will care. If a computer fells a tree in the woods, it doesn't make a sound. I wouldn't discount the possibility, though, that a future "creative" computer manages to produce a proof indecipherable to humans of a theorem we care about, at which point I think there will be quite a perturbation in the mathematical community. If a computer proves the Riemann Hypothesis in such a way that no one can understand it, but it spits out a Coq document that everyone can load and verify, will people consider the problem solved?

Retra 11y ago
The problem will be solved when any other problems that depend on its solution become solvable.
johncolanduoni 11y ago
> If a computer proves the Riemann Hypothesis in such a way that no one can understand it, but it spits out a Coq document that everyone can load and verify, will people consider the problem solved? We've already seen this play out to a certain degree with the proof of the four color theorem[1]. Basically, the problem was reduced to checking about 2000 specific graphs (the checked property was more complex than simple colorability). The reduction part was very complex but still checked by humans, but checking the ~2000 graphs was a computationally expensive process that took computers thousands of hours to complete, which was completely infeasible for direct human verification. There was a lot of controversy over whether this counted as a proof. Since then the proof has been simplified to 600 special cases and run through a proper proof assistant (Coq), so it is now pretty widely accepted as proved. It's not quite analogous since the core of the proof was still human created and checked, and the basic form of the computer generated portions was well understood (i.e. the kinds of steps they used). There is some extra doubt involved when this is not the case, since it's possible the computer came up with a novel proof of inconsistency if we don't know at all how the individual parts of the proof work. [1]: https://en.wikipedia.org/wiki/Four_color_theorem https://en.wikipedia.org/wiki/Four_color_theorem
jnwrd 11y ago
Some portion of what is deemed important arises from the interaction between mathematics and physics. It would be fascinating to automate the invention of new mathematical structures and then have a post-human physicist try to apply these new structures.
DubiousPusher 11y ago
>>I wouldn't discount the possibility, though, that a future "creative" computer manages to produce a proof indecipherable to humans... How would this be so? The sheer length of the proof rendering it unverifiable in a human lifespan?
- marcelluspye 11y ago
  I had written what now seems to me to be an unnecessarily long response to this, but along the way I think I thought of an example to demonstrate my point: Shinichi Mochizuki spent several years compiling a large body of work which he calls "Inter-Universal Teichmuller Theory" which which implies a number of important results in number theory, algebraic geometry, and other areas (if I understand the gist of it). However, he has run into a wall in the mathematical community in that almost no one wants to spend the time to try to understand what he wrote (I believe he said he believes it would take someone well-versed in the field around 6 months of study to get a grasp of it). If a human could produce enough work in sufficiently dense terms that other mathematicians don't want to touch it, I can imagine a computer could generate exponentially more work in a much less human-readable format than Mochizuki (albeit formally correct).
joe_the_user 11y ago
The main thing I'd say is that either the quality of "creativity" is something that effectively duplicates (or even extends) the human notion of creativity or it's something arbitrary that there could be a way for us to care about. Even if someone formulated an apparently human-independent mathematical statement of "interesting", you would still the human judgment that this was credible.
ep103 11y ago
so basically, unit testing for all of mathematics?

Retra 11y ago

The problem will be solved when any other problems that depend on its solution become solvable.

johncolanduoni 11y ago

> If a computer proves the Riemann Hypothesis in such a way that no one can understand it, but it spits out a Coq document that everyone can load and verify, will people consider the problem solved? We've already seen this play out to a certain degree with the proof of the four color theorem[1]. Basically, the problem was reduced to checking about 2000 specific graphs (the checked property was more complex than simple colorability). The reduction part was very complex but still checked by humans, but checking the ~2000 graphs was a computationally expensive process that took computers thousands of hours to complete, which was completely infeasible for direct human verification. There was a lot of controversy over whether this counted as a proof. Since then the proof has been simplified to 600 special cases and run through a proper proof assistant (Coq), so it is now pretty widely accepted as proved. It's not quite analogous since the core of the proof was still human created and checked, and the basic form of the computer generated portions was well understood (i.e. the kinds of steps they used). There is some extra doubt involved when this is not the case, since it's possible the computer came up with a novel proof of inconsistency if we don't know at all how the individual parts of the proof work. [1]: https://en.wikipedia.org/wiki/Four_color_theorem https://en.wikipedia.org/wiki/Four_color_theorem

jnwrd 11y ago

Some portion of what is deemed important arises from the interaction between mathematics and physics. It would be fascinating to automate the invention of new mathematical structures and then have a post-human physicist try to apply these new structures.

DubiousPusher 11y ago

>>I wouldn't discount the possibility, though, that a future "creative" computer manages to produce a proof indecipherable to humans... How would this be so? The sheer length of the proof rendering it unverifiable in a human lifespan?

marcelluspye 11y ago
I had written what now seems to me to be an unnecessarily long response to this, but along the way I think I thought of an example to demonstrate my point: Shinichi Mochizuki spent several years compiling a large body of work which he calls "Inter-Universal Teichmuller Theory" which which implies a number of important results in number theory, algebraic geometry, and other areas (if I understand the gist of it). However, he has run into a wall in the mathematical community in that almost no one wants to spend the time to try to understand what he wrote (I believe he said he believes it would take someone well-versed in the field around 6 months of study to get a grasp of it). If a human could produce enough work in sufficiently dense terms that other mathematicians don't want to touch it, I can imagine a computer could generate exponentially more work in a much less human-readable format than Mochizuki (albeit formally correct).

joe_the_user 11y ago

The main thing I'd say is that either the quality of "creativity" is something that effectively duplicates (or even extends) the human notion of creativity or it's something arbitrary that there could be a way for us to care about. Even if someone formulated an apparently human-independent mathematical statement of "interesting", you would still the human judgment that this was credible.

ep103 11y ago

so basically, unit testing for all of mathematics?