3 ms·

Given incompleteness and like the difficulty of the busy beaver problem, its pretty clear why brute forcing isn't really effective for much of math. Plus, the r

Given incompleteness and like the difficulty of the busy beaver problem, its pretty clear why brute forcing isn't really effective for much of math. Plus, the results it gives are maybe a bit less interesting because they don't provide as much insight on a clean and simple structure. How math works is cool and all, but why path works can open many new insights.

dhosek 6y ago
On the flip side, the computer proof at least resolves the question of whether a given conjecture is true. The proof of the four color theorem by computer in 1976–89 opened the door to simplifications and clarifications of the proof in the decade following. This is not unlike a lot of the difficult proofs of the last century. The receommended path to understanding Wiles's proof of Fermat's Last Theorem begins with Yves Hellegouach's book, Invitation to the Mathematics of Fermat Wiles http://www.amazon.com/exec/obidos/ASIN/0123392519/donhosek http://www.amazon.com/exec/obidos/ASIN/0123392519/donhosek and then Gary Cornell's Modular Forms and Fermat's Last Theorem http://www.amazon.com/exec/obidos/ASIN/0387946098/donhosek http://www.amazon.com/exec/obidos/ASIN/0387946098/donhosek which assumes a graduate student's understanding of number theory and then the reader is ready to actually read Wiles. When I was in grad school, I remember reading a comment from someone talking about looking at her roommate's materials for her PhD in English and realizing that while what she had was comprehensible to her even if she didn't necessarily understand any of it, her own materials for her math PhD were completely unintelligible to outsiders.
- sukilot 6y ago
  Users of English constantly generate new low hanging fruit for research. In math, any low hanging fruit orchard becomes a non-mathematical science.
Ericson2314 6y ago
Do you really think humans have some magic powers for doing computationally intractable proof search?? Do you think human-written proofs vs machine-written proofs magically overcome what Gödel points out a limitation of the language itself both proofs are written in (or, in principle, "compile to")?? Why so much of this human skills mysticism on HN of all places... :/
- codr7 6y ago
  Because many of us deal with computers all day and realize deep down there is a fundamental difference between humans and computers that isn't going anywhere?
  - kadoban 6y ago
    It's not going anywhere until it does. Look at the history of AI in various tasks and fields. It only ever goes one direction, and there does not seem to be a fundamental block.
    - codr7 6y ago
      I'd argue that the fundamental block is that it's not human, period.
      - kadoban 6y ago
        We appear to exist in a mechanical universe of laws. There's really no way it's possible both that humans exist and that we can't replicate or approximate enough parts of the human brain enough to match or better human reasoning. If the human part bothers you, substitute animals instead. They do much of what we need to various, usually somewhat lesser levels. This line of thinking is reinforced by the results we've had so far. Why should we assume there's a limit if we haven't hit one yet, and see no fundamental block? Where would this limit be? Even our extremely limited understanding so far has provided some pretty amazing results. The only question is performance and difficulty at various levels of technology and understanding. It's a matter of time. It won't be tomorrow, but unless we cease to exist first, it will happen. And once it's a matter of engineering that can be iterated upon, things get really interesting.
        codr7 6y ago
        I realize I'm most probably not going to change your mind here :) And it's fine, live and let live. I've had plenty of experiences in meditation and on hallucinogenics that don't fit into your picture. What I don't understand is how you can be so certain of anything, given that we're all observing the system subjectively from the inside.
EE84M3i 6y ago
>Given incompleteness and like the difficulty of the busy beaver problem I'm confused. Could you explain what these have to do with the topic at hand? They seem orthogonal.
- sukilot 6y ago
  An arbitrary problem is most likely be either trivial or many orders of magnitude too hard for a computer, not solvable in the tiny range of scale that a computer can handle. No matter how many computations your computer can do in a decade, almost every calculation is bigger than that.
  - EE84M3i 6y ago
    Sure, but as far as I know, for neither the busy beaver problem nor godel's incompleteness are the capabilities that humans bring to the table different than computers.

dhosek 6y ago

On the flip side, the computer proof at least resolves the question of whether a given conjecture is true. The proof of the four color theorem by computer in 1976–89 opened the door to simplifications and clarifications of the proof in the decade following. This is not unlike a lot of the difficult proofs of the last century. The receommended path to understanding Wiles's proof of Fermat's Last Theorem begins with Yves Hellegouach's book, Invitation to the Mathematics of Fermat Wiles http://www.amazon.com/exec/obidos/ASIN/0123392519/donhosek http://www.amazon.com/exec/obidos/ASIN/0123392519/donhosek and then Gary Cornell's Modular Forms and Fermat's Last Theorem http://www.amazon.com/exec/obidos/ASIN/0387946098/donhosek http://www.amazon.com/exec/obidos/ASIN/0387946098/donhosek which assumes a graduate student's understanding of number theory and then the reader is ready to actually read Wiles. When I was in grad school, I remember reading a comment from someone talking about looking at her roommate's materials for her PhD in English and realizing that while what she had was comprehensible to her even if she didn't necessarily understand any of it, her own materials for her math PhD were completely unintelligible to outsiders.

sukilot 6y ago
Users of English constantly generate new low hanging fruit for research. In math, any low hanging fruit orchard becomes a non-mathematical science.

Ericson2314 6y ago

Do you really think humans have some magic powers for doing computationally intractable proof search?? Do you think human-written proofs vs machine-written proofs magically overcome what Gödel points out a limitation of the language itself both proofs are written in (or, in principle, "compile to")?? Why so much of this human skills mysticism on HN of all places... :/

codr7 6y ago
Because many of us deal with computers all day and realize deep down there is a fundamental difference between humans and computers that isn't going anywhere?
- kadoban 6y ago
  It's not going anywhere until it does. Look at the history of AI in various tasks and fields. It only ever goes one direction, and there does not seem to be a fundamental block.
  - codr7 6y ago
    I'd argue that the fundamental block is that it's not human, period.
    - kadoban 6y ago
      We appear to exist in a mechanical universe of laws. There's really no way it's possible both that humans exist and that we can't replicate or approximate enough parts of the human brain enough to match or better human reasoning. If the human part bothers you, substitute animals instead. They do much of what we need to various, usually somewhat lesser levels. This line of thinking is reinforced by the results we've had so far. Why should we assume there's a limit if we haven't hit one yet, and see no fundamental block? Where would this limit be? Even our extremely limited understanding so far has provided some pretty amazing results. The only question is performance and difficulty at various levels of technology and understanding. It's a matter of time. It won't be tomorrow, but unless we cease to exist first, it will happen. And once it's a matter of engineering that can be iterated upon, things get really interesting.
      - codr7 6y ago
        I realize I'm most probably not going to change your mind here :) And it's fine, live and let live. I've had plenty of experiences in meditation and on hallucinogenics that don't fit into your picture. What I don't understand is how you can be so certain of anything, given that we're all observing the system subjectively from the inside.

EE84M3i 6y ago

>Given incompleteness and like the difficulty of the busy beaver problem I'm confused. Could you explain what these have to do with the topic at hand? They seem orthogonal.

sukilot 6y ago
An arbitrary problem is most likely be either trivial or many orders of magnitude too hard for a computer, not solvable in the tiny range of scale that a computer can handle. No matter how many computations your computer can do in a decade, almost every calculation is bigger than that.
- EE84M3i 6y ago
  Sure, but as far as I know, for neither the busy beaver problem nor godel's incompleteness are the capabilities that humans bring to the table different than computers.