3 ms·

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

by 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.
  - Tainnor 3y ago
    You should look up provable security. And also, while security proofs typically rely on unproven assumptions, correctness proofs in cryptography are "regular" proofs for all intents and purposes. You can't even do RSA etc. without understanding prime numbers which is impossible if you limit yourself to propositional calculus ("SAT"). > 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. This is false.

by js8 3y ago

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.
- Tainnor 3y ago
  You should look up provable security. And also, while security proofs typically rely on unproven assumptions, correctness proofs in cryptography are "regular" proofs for all intents and purposes. You can't even do RSA etc. without understanding prime numbers which is impossible if you limit yourself to propositional calculus ("SAT"). > 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. This is false.