8 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 re

> 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.
- constantcrying 3y ago
  None of this is true and your understanding of the subject is obviously very poor.
  - js8 3y ago
    Before there was AlphaGo, many top Go players believed that understanding Go is somehow special in helping us to understand the universe. The AlphaGo was a shock, because it turned Go into "just another game", which can be beaten by enough calculations on a powerful computer. I think the mathematics is the same. Lot of its beauty we cherish, because we don't properly understand it on the "raw" level of SAT (I would write logic, but I really mean the simplest metalogic you need), which is evidenced by our lack of understanding of P vs NP. Once it is understood, the process of "doing math" will be understood algorithmically, and it will become "boring" or "dull". But as I said, I don't think lack of universal meaning (or lack of mystique) has to detract from the beauty of mathematics.
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.

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.
constantcrying 3y ago
None of this is true and your understanding of the subject is obviously very poor.
- js8 3y ago
  Before there was AlphaGo, many top Go players believed that understanding Go is somehow special in helping us to understand the universe. The AlphaGo was a shock, because it turned Go into "just another game", which can be beaten by enough calculations on a powerful computer. I think the mathematics is the same. Lot of its beauty we cherish, because we don't properly understand it on the "raw" level of SAT (I would write logic, but I really mean the simplest metalogic you need), which is evidenced by our lack of understanding of P vs NP. Once it is understood, the process of "doing math" will be understood algorithmically, and it will become "boring" or "dull". But as I said, I don't think lack of universal meaning (or lack of mystique) has to detract from the beauty of mathematics.

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.