4 ms·

IMHO it's even worse. Once we figure out P vs NP, we will understand what it means to invert boolean functions algorithmically, and all mathematics will be repl

by js8 3y ago

IMHO it's even worse. Once we figure out P vs NP, we will understand what it means to invert boolean functions algorithmically, and all mathematics will be replaced with an automated process. Today, most of the math is figuring out how to solve an equation, i.e. to give an algorithm to calculate the solution. We then "quantize" the algorithm to a state machine (e.g. convert reals to floats, algorithm steps to machine code), so that we could run the state machine on a computer and get a result. However, once you know what it takes to invert boolean functions, you don't need the solution step, you can just quantize your equation (problem) directly to a SAT instance, and let the inversion algorithm do all the hard work. No (elegant and readable) math is required anymore. So I think we better treat mathematics as a "useless" human artifact (like art or chess) rather than something of practical value.

yau8edq12i 3y ago
> IMHO it's even worse. Once we figure out P vs NP, we will understand what it means to invert boolean functions algorithmically, and all mathematics will be replaced with an automated process. I'm sorry, but that's just naive techno-solutionism. Maybe the computer will be able to solve your syntax problems, i.e., write proofs. It will never know anything about the semantics. Said differently. Maybe the computer will be able to give you a proof on demand on statement number 123456789 in some Gödel numbering of statements. What it won't be able to tell you is that the theorem should be called the "intermediate value theorem" and what it means. Math isn't just coming up with formally correct proofs for pre-existing statements. I also don't see what "P vs NP" has to do with anything. > Today, most of the math is figuring out how to solve an equation, i.e. to give an algorithm to calculate the solution. We then "quantize" the algorithm to a state machine (e.g. convert reals to floats, algorithm steps to machine code), so that we could run the state machine on a computer and get a result. I'm a mathematician. What you wrote is just bonkers. Some parts of math are about writing algorithms to solve equations. The vast majority of math isn't.
- js8 3y ago
  My point is, the need for semantics is a human construct, it's not required to solve practical problems. Practical value of MVT is that we can apply it in the process of describing a solution, i.e. an algorithm. But if you have a SAT algorithm that can somehow inherently apply a finite instance of MVT, you no longer need to know what MVT is. And this is at the heart of P vs NP question, how to solve SAT, and once we understand that, all the math that is about solving equations (i.e. that of practical value) will become very boring. Kinda like when a game becomes solved with a computer. (This reminds me of Chomsky and Norvig debate on the machine learning and nature of understanding. I wouldn't think I would take Norvig's position, yet here we are.) Addendum: I am also not arguing that computers writing proofs are a necessity for this, but rather efficiently (as possible) solving SAT instances. You don't need to state a hypothesis (and thus prove it) for an infinite number of cases to solve practical problems. I am also not judging value of math - yeah, it is fun. All I am saying it inherently has a human dimension in the sense we don't need it (assuming we have an efficient SAT solver) to solve practical problems.
  - seanhunter 3y ago
    Most equations that can be solved can already be solved symbolically by things like mathematica or numerically by a grab-bag of numerical techniques that every maths, engineering and physics student learns at some point. You don't need to have found the solution to P vs NP to do any of that. I think most mathematicians would say that most of maths is not in solving equations because once you get the right equations, solving them is a simple mechanical process for the most part. Most of maths is figuring out what the right equations are in the first place and proving that what you have done is legitimate.
    - js8 3y ago
      I disagree that converting from an equation to a solution algorithm is a straightforward process. It is very much where mathematics helps, for example just to ensure convergence of the method. Also, the way you model reality (choose the equation) is often done with the limitations of solvability in mind. I also disagree that maths can help you pick the right equations, just like there is no formal method that can verify whether a program specification is appropriate to the problem. Equation (or a model) is just an infinite family of SAT problems, typically parametrized on our understanding what a "number" is. If we had a really good SAT solver, then getting a solution would indeed be a really straightforward process (just pick the number representation) of solving the instance. The same is also true for checking "legitimacy" (which I interpret as consistency) of the model - SAT solver would tell you that the instance is unsatisfiable and why. But you can never formally determine that the chosen SAT instance is appropriate model for the task at hand.
- curtainsforus 3y ago
  Strange, for you to say this in the age of transformers. They are obviously not there yet, but it seems inevitable to me that e.g. gpt 'understands' things better than a markov chain, and that future systems will understand more.
  - js8 3y ago
    I know you're responding to someone else, but funny you say that. I suspect modern NN's are just iteratively solving some really large instances of SAT (similar to WalkSAT), to find a representation of a circuit that best matches a function defined on training examples (which are the constraints). So they're, unwittingly, kinda the SotA SAT solvers.
constantcrying 3y ago
>IMHO it's even worse. Once we figure out P vs NP, we will understand what it means to invert boolean functions algorithmically, and all mathematics will be replaced with an automated process. Literal nonsense. Do you not realize that P vs. NP might have a negative outcome (extremely likely)? >Today, most of the math is figuring out how to solve an equation, i.e. to give an algorithm to calculate the solution. Plainly false. In basically any field proving the existence of a solution is far, far harder than calculating the solution numerically. See e.g. PDEs. >We then "quantize" the algorithm to a state machine (e.g. convert reals to floats, algorithm steps to machine code), so that we could run the state machine on a computer and get a result. Literally not true. Not even the assumption is right.
- js8 3y ago
  > Do you not realize that P vs. NP might have a negative outcome (extremely likely) The outcome will matter less than having an answer. And I do think it will be a negative outcome either way, because it will obsolete lot of beautiful math, and replace it with a more mechanical process. > In basically any field proving the existence of a solution is far, far harder than calculating the solution numerically. First of all, if you want to ascertain whether the numerical algorithm works correctly, you have to prove the existence of the solution. That's part of the (equation -> solution algorithm) conversion process. Now, you can possibly get by without proving existence of the solution for the infinite family (and confront the numerical solution directly with reality). But doing that is more complicated than, assuming there is a SAT solver, plug the SAT instance into it and see if there is a solution (and you can get, for a finite family of instances, a similar guarantee you would get from the existence proof). > Not even the assumption is right. Not sure what assumption you refer to. Computers don't run algorithms (because algorithms handle unbounded input/output), computers are just a very large state machines. So you need to convert the algorithm to a state machine first. Saying "run algorithm on a computer" is just a useful figure of speech, but somewhat misleading, because it implies certain quantization.
  - constantcrying 3y ago
    >The outcome will matter less than having an answer. And I do think it will be a negative outcome either way, because it will obsolete lot of beautiful math, and replace it with a more mechanical process. The negative outcome will have exactly zero implications about anything. Except "turns out we were right all along" polynomial problems are just fundamentally less hard than problems you can verify the solution of in polynomial time. This has ZERO implications on anyone, except the mathematicians who prove it, who will get a price and quite a bit of academic fame. That is literally it. >But doing that is more complicated than, assuming there is a SAT solver, plug the SAT instance into it and see if there is a solution (and you can get, for a finite family of instances, a similar guarantee you would get from the existence proof). Even is SAT is P that doesn't imply a solution can feasibly be found. And if P neq NP, then SAT might not be P.
Tainnor 3y ago
That's some of the most confidently written nonsense I've read in a while. > all mathematics will be replaced with an automated process FOL is undecidable, so we know this is impossible.
- js8 3y ago
  I think you miss the point. I am not disputing FOL being undecidable. What I am saying is that, once we know how to solve SAT well enough, most mathematics will become obsolete (especially for applications). It will be obsoleted the similar way that symbolic solving of equations got obsoleted with numerical solving, once computers (and numerical algorithms) became prevalent enough. Practically minded people will simply skip logical proofs and model the world directly with SAT instances. Mathematics will remain an intellectual curiosity. In a way, I agree with the article - what makes math interesting is the human perspective and creativity. But I believe it's "worse" - taken objectively, math is actually pretty boring and there is only little depth.
  - Tainnor 3y ago
    > symbolic solving of equations got obsoleted with numerical solving That never happened, symbolic and numerical mathematics coexist to this day. Cryptography, for example, relies on exact arithmetic. On that note, good luck trying to solve problems in cryptography with "SAT instances".
    - js8 3y ago
      Again, you miss the point, there will be a paradigm shift. Yes, symbolic maths still exists, but nobody is looking up a special function to solve an equation. They just plug the numbers (and the state machine approximation of the numerical operations) in the computer and numerically, the result comes out. Symbolic/numeric is just analogy of the paradigm shift that will come to all (applied) math. Another example is in statistics, shift from parametric to non-parametric. Cryptography.. relies on unproven belief in ETH or P/=NP or some such (in fact, cryptography has, since Caesar, relied on unproven beliefs about cryptosystems). But that's just a belief, we don't really understand how hard any of these specific problems are. Which is actually a great example of the new paradigm I am talking about, because it shows we don't need proofs (of statements about infinitely many things). We can just quantize things directly (into a state machine that actually does the crypto stuff) and be happy. We haven't even scratched the surface of what is possible in P vs NP. In particular, CNF representation of SAT instances might be a really crappy one.

by js8 3y ago

yau8edq12i 3y ago

> IMHO it's even worse. Once we figure out P vs NP, we will understand what it means to invert boolean functions algorithmically, and all mathematics will be replaced with an automated process. I'm sorry, but that's just naive techno-solutionism. Maybe the computer will be able to solve your syntax problems, i.e., write proofs. It will never know anything about the semantics. Said differently. Maybe the computer will be able to give you a proof on demand on statement number 123456789 in some Gödel numbering of statements. What it won't be able to tell you is that the theorem should be called the "intermediate value theorem" and what it means. Math isn't just coming up with formally correct proofs for pre-existing statements. I also don't see what "P vs NP" has to do with anything. > Today, most of the math is figuring out how to solve an equation, i.e. to give an algorithm to calculate the solution. We then "quantize" the algorithm to a state machine (e.g. convert reals to floats, algorithm steps to machine code), so that we could run the state machine on a computer and get a result. I'm a mathematician. What you wrote is just bonkers. Some parts of math are about writing algorithms to solve equations. The vast majority of math isn't.

js8 3y ago
My point is, the need for semantics is a human construct, it's not required to solve practical problems. Practical value of MVT is that we can apply it in the process of describing a solution, i.e. an algorithm. But if you have a SAT algorithm that can somehow inherently apply a finite instance of MVT, you no longer need to know what MVT is. And this is at the heart of P vs NP question, how to solve SAT, and once we understand that, all the math that is about solving equations (i.e. that of practical value) will become very boring. Kinda like when a game becomes solved with a computer. (This reminds me of Chomsky and Norvig debate on the machine learning and nature of understanding. I wouldn't think I would take Norvig's position, yet here we are.) Addendum: I am also not arguing that computers writing proofs are a necessity for this, but rather efficiently (as possible) solving SAT instances. You don't need to state a hypothesis (and thus prove it) for an infinite number of cases to solve practical problems. I am also not judging value of math - yeah, it is fun. All I am saying it inherently has a human dimension in the sense we don't need it (assuming we have an efficient SAT solver) to solve practical problems.
- seanhunter 3y ago
  Most equations that can be solved can already be solved symbolically by things like mathematica or numerically by a grab-bag of numerical techniques that every maths, engineering and physics student learns at some point. You don't need to have found the solution to P vs NP to do any of that. I think most mathematicians would say that most of maths is not in solving equations because once you get the right equations, solving them is a simple mechanical process for the most part. Most of maths is figuring out what the right equations are in the first place and proving that what you have done is legitimate.
  - js8 3y ago
    I disagree that converting from an equation to a solution algorithm is a straightforward process. It is very much where mathematics helps, for example just to ensure convergence of the method. Also, the way you model reality (choose the equation) is often done with the limitations of solvability in mind. I also disagree that maths can help you pick the right equations, just like there is no formal method that can verify whether a program specification is appropriate to the problem. Equation (or a model) is just an infinite family of SAT problems, typically parametrized on our understanding what a "number" is. If we had a really good SAT solver, then getting a solution would indeed be a really straightforward process (just pick the number representation) of solving the instance. The same is also true for checking "legitimacy" (which I interpret as consistency) of the model - SAT solver would tell you that the instance is unsatisfiable and why. But you can never formally determine that the chosen SAT instance is appropriate model for the task at hand.
curtainsforus 3y ago
Strange, for you to say this in the age of transformers. They are obviously not there yet, but it seems inevitable to me that e.g. gpt 'understands' things better than a markov chain, and that future systems will understand more.
- js8 3y ago
  I know you're responding to someone else, but funny you say that. I suspect modern NN's are just iteratively solving some really large instances of SAT (similar to WalkSAT), to find a representation of a circuit that best matches a function defined on training examples (which are the constraints). So they're, unwittingly, kinda the SotA SAT solvers.

constantcrying 3y ago

>IMHO it's even worse. Once we figure out P vs NP, we will understand what it means to invert boolean functions algorithmically, and all mathematics will be replaced with an automated process. Literal nonsense. Do you not realize that P vs. NP might have a negative outcome (extremely likely)? >Today, most of the math is figuring out how to solve an equation, i.e. to give an algorithm to calculate the solution. Plainly false. In basically any field proving the existence of a solution is far, far harder than calculating the solution numerically. See e.g. PDEs. >We then "quantize" the algorithm to a state machine (e.g. convert reals to floats, algorithm steps to machine code), so that we could run the state machine on a computer and get a result. Literally not true. Not even the assumption is right.

js8 3y ago
> Do you not realize that P vs. NP might have a negative outcome (extremely likely) The outcome will matter less than having an answer. And I do think it will be a negative outcome either way, because it will obsolete lot of beautiful math, and replace it with a more mechanical process. > In basically any field proving the existence of a solution is far, far harder than calculating the solution numerically. First of all, if you want to ascertain whether the numerical algorithm works correctly, you have to prove the existence of the solution. That's part of the (equation -> solution algorithm) conversion process. Now, you can possibly get by without proving existence of the solution for the infinite family (and confront the numerical solution directly with reality). But doing that is more complicated than, assuming there is a SAT solver, plug the SAT instance into it and see if there is a solution (and you can get, for a finite family of instances, a similar guarantee you would get from the existence proof). > Not even the assumption is right. Not sure what assumption you refer to. Computers don't run algorithms (because algorithms handle unbounded input/output), computers are just a very large state machines. So you need to convert the algorithm to a state machine first. Saying "run algorithm on a computer" is just a useful figure of speech, but somewhat misleading, because it implies certain quantization.
- constantcrying 3y ago
  >The outcome will matter less than having an answer. And I do think it will be a negative outcome either way, because it will obsolete lot of beautiful math, and replace it with a more mechanical process. The negative outcome will have exactly zero implications about anything. Except "turns out we were right all along" polynomial problems are just fundamentally less hard than problems you can verify the solution of in polynomial time. This has ZERO implications on anyone, except the mathematicians who prove it, who will get a price and quite a bit of academic fame. That is literally it. >But doing that is more complicated than, assuming there is a SAT solver, plug the SAT instance into it and see if there is a solution (and you can get, for a finite family of instances, a similar guarantee you would get from the existence proof). Even is SAT is P that doesn't imply a solution can feasibly be found. And if P neq NP, then SAT might not be P.

Tainnor 3y ago

That's some of the most confidently written nonsense I've read in a while. > all mathematics will be replaced with an automated process FOL is undecidable, so we know this is impossible.

js8 3y ago
I think you miss the point. I am not disputing FOL being undecidable. What I am saying is that, once we know how to solve SAT well enough, most mathematics will become obsolete (especially for applications). It will be obsoleted the similar way that symbolic solving of equations got obsoleted with numerical solving, once computers (and numerical algorithms) became prevalent enough. Practically minded people will simply skip logical proofs and model the world directly with SAT instances. Mathematics will remain an intellectual curiosity. In a way, I agree with the article - what makes math interesting is the human perspective and creativity. But I believe it's "worse" - taken objectively, math is actually pretty boring and there is only little depth.
- Tainnor 3y ago
  > symbolic solving of equations got obsoleted with numerical solving That never happened, symbolic and numerical mathematics coexist to this day. Cryptography, for example, relies on exact arithmetic. On that note, good luck trying to solve problems in cryptography with "SAT instances".
  - js8 3y ago
    Again, you miss the point, there will be a paradigm shift. Yes, symbolic maths still exists, but nobody is looking up a special function to solve an equation. They just plug the numbers (and the state machine approximation of the numerical operations) in the computer and numerically, the result comes out. Symbolic/numeric is just analogy of the paradigm shift that will come to all (applied) math. Another example is in statistics, shift from parametric to non-parametric. Cryptography.. relies on unproven belief in ETH or P/=NP or some such (in fact, cryptography has, since Caesar, relied on unproven beliefs about cryptosystems). But that's just a belief, we don't really understand how hard any of these specific problems are. Which is actually a great example of the new paradigm I am talking about, because it shows we don't need proofs (of statements about infinitely many things). We can just quantize things directly (into a state machine that actually does the crypto stuff) and be happy. We haven't even scratched the surface of what is possible in P vs NP. In particular, CNF representation of SAT instances might be a really crappy one.