5 ms·

> The solution required modern techniques and computer algorithms. “Twenty years ago, [this question] was absolutely out of reach; 10 years ago it would require

> The solution required modern techniques and computer algorithms. “Twenty years ago, [this question] was absolutely out of reach; 10 years ago it would require an enormous effort of writing all necessary software, so only now all the factors came together,” wrote Anton Zorich, of the Institute of Mathematics of Jussieu in Paris, in an email. Right here is the most interesting part of the article for me. It's definitely cool that we're making these sorts of discoveries still, but it's more interesting how so many more problems are now being solved via computer. Had I gone all the way through my PhD (in math), I'd be some combination of worried that my computing skills were up to snuff, and intrigued about the increasing role of computers in mathematics.

deleted 6y ago
[deleted]
xxpor 6y ago
Given most of us carry a computer with us at all times that by itself can do billions of calculations a second, I'd be more concerned/intrigued if this kind of stuff WASN'T being solved by computers these days. Even if it's just for brute forcing, that's obviously a lot more practical with computers than if we were doing stuff by hand or slide rule.
- kazagistar 6y ago
  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.
  - 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.
coliveira 6y ago
The fact that these mathematical problems can be solved by computer doesn't mean that any computer scientist or teenage hacker can go around solving math problems. The solution to these problems is more a matter of mathematical skill combined with some programming than a purely programming effort. So I don't think that mathematicians have any reason to fear for their jobs, they just have another tool to learn to be good at what they do.
- kmill 6y ago
  I think of computers as being telescopes for math. They can help you see deeper than you could before, but you still need to know where to look, make sure you have enough resolving power, etc.
- pessimizer 6y ago
  Any computer scientist or teenage hacker could always go around solving math problems. I actually think that being able to afford access to computer power makes the problems amenable to computing power less accessible to outsiders. All outsiders needed before was access to a good library, and now all they need is access to archive.org, library genesis and sci-hub.
- wmeredith 6y ago
  Thanks for pointing this out so eloquently. The computer is a lever. You still have to know how to apply it.
dhosek 6y ago
It's worth noting that computer-assisted proofs date back to 1976 with the proof of the four-color theorem (although it turned out that it was another thirteen years before all the flaws and gaps were resolved).
- ChrisLomont 6y ago
  They date back much further. McCarthy in the 1960s, and over a half dozen groups by 1970, had developed computer assisted proof tools that were proving theorems. The 4 color theorem in 1976 was just a very famous example. I think Turing (30s? 40s?) and later von Neumann (50s) also did some computer assisted theorem proving, but I’d have to dig for precise references.
thomasahle 6y ago
While computer proofs are better than no proofs at all, they aren't as exciting as "classic" proofs, which typically build new theory and inspire new questions to be solved.
- Ericson2314 6y ago
  The 4 color theorem was a boring case analysis, but that doesn't mean that all computer proofs are boring and tedious. We have proof assistants using many beautiful type theoretic languages, and tools which can (attempt) to write proofs in this languages. In fact, this is one of the best usages of ML because we hardly care whatever impenetrable bullshit goes into the proof search when the proof must be self-justifying, and, just like a ML go game log, potentially lead to new techniques for human mathematicians.
Waterluvian 6y ago
If you watch many mathematicians on YouTube a lot of them are just hunt and peck Pythonistas. It’s perfectly fine when the code is the tool, not the product.
- mhh__ 6y ago
  > hunt and peck Pythonistas The real curse seems to be MATLAB in my experience. No engineering book is incomplete without an untested, uncommented, unindented MATLAB code listing at the back. I don't like Python, but at least it forces you to write somewhat legible code. Luckily it usually doesn't matter, but when you have things like COVID-19 models written in this matter I fear for the worst.

deleted 6y ago

[deleted]

xxpor 6y ago

Given most of us carry a computer with us at all times that by itself can do billions of calculations a second, I'd be more concerned/intrigued if this kind of stuff WASN'T being solved by computers these days. Even if it's just for brute forcing, that's obviously a lot more practical with computers than if we were doing stuff by hand or slide rule.

kazagistar 6y ago
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.
- 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.

coliveira 6y ago

The fact that these mathematical problems can be solved by computer doesn't mean that any computer scientist or teenage hacker can go around solving math problems. The solution to these problems is more a matter of mathematical skill combined with some programming than a purely programming effort. So I don't think that mathematicians have any reason to fear for their jobs, they just have another tool to learn to be good at what they do.

kmill 6y ago
I think of computers as being telescopes for math. They can help you see deeper than you could before, but you still need to know where to look, make sure you have enough resolving power, etc.
pessimizer 6y ago
Any computer scientist or teenage hacker could always go around solving math problems. I actually think that being able to afford access to computer power makes the problems amenable to computing power less accessible to outsiders. All outsiders needed before was access to a good library, and now all they need is access to archive.org, library genesis and sci-hub.
wmeredith 6y ago
Thanks for pointing this out so eloquently. The computer is a lever. You still have to know how to apply it.

dhosek 6y ago

It's worth noting that computer-assisted proofs date back to 1976 with the proof of the four-color theorem (although it turned out that it was another thirteen years before all the flaws and gaps were resolved).

ChrisLomont 6y ago
They date back much further. McCarthy in the 1960s, and over a half dozen groups by 1970, had developed computer assisted proof tools that were proving theorems. The 4 color theorem in 1976 was just a very famous example. I think Turing (30s? 40s?) and later von Neumann (50s) also did some computer assisted theorem proving, but I’d have to dig for precise references.

thomasahle 6y ago

While computer proofs are better than no proofs at all, they aren't as exciting as "classic" proofs, which typically build new theory and inspire new questions to be solved.

Ericson2314 6y ago
The 4 color theorem was a boring case analysis, but that doesn't mean that all computer proofs are boring and tedious. We have proof assistants using many beautiful type theoretic languages, and tools which can (attempt) to write proofs in this languages. In fact, this is one of the best usages of ML because we hardly care whatever impenetrable bullshit goes into the proof search when the proof must be self-justifying, and, just like a ML go game log, potentially lead to new techniques for human mathematicians.

Waterluvian 6y ago

If you watch many mathematicians on YouTube a lot of them are just hunt and peck Pythonistas. It’s perfectly fine when the code is the tool, not the product.

mhh__ 6y ago
> hunt and peck Pythonistas The real curse seems to be MATLAB in my experience. No engineering book is incomplete without an untested, uncommented, unindented MATLAB code listing at the back. I don't like Python, but at least it forces you to write somewhat legible code. Luckily it usually doesn't matter, but when you have things like COVID-19 models written in this matter I fear for the worst.