3 ms·

I definitely mean semantics. I mean LaTeX can do syntax very easily. Let's narrow down the scope. Suppose in an alternate history, we don't know the quadratic

I definitely mean semantics. I mean LaTeX can do syntax very easily. Let's narrow down the scope. Suppose in an alternate history, we don't know the quadratic formula, but yet we see graphically that there are zeroes. We suck at writing proofs, so we set out to find a formula using software to "scan the search space". We have a sample of 10^6 quadratic equations and we will believe our program if it solves all of them within a floating-point epsilon. So given those constraints, we agree to try, say 10 billion unique, randomly generated "math tokens". Would we discover the quadratic formula? this is what interests me. I know it won't work the other way around (scanning n billion doesn't mean there isn't a solution). But this is an example of my question, can we trade cpu for knowledge/proofs? (I dont know why I said imperative languages, that's probably an irrelevant question detail. I'm more concerned about the general case).

zamadatix 3y ago
The problem is we can't believe things like "we sampled the first 10^6 examples we came up with and it held so we can trust it to be valid". These are still just conjectures and sometimes turn out to be false at extreme bounds or corner cases. This doesn't mean conjectures (or even known sometimes-false approximations) are useless, it's just a different discussion vs what is trying to be done with these tools. One case you can get away with this is exhaustively checking the ENTIRE search space. E.g. I can prove an 8 bit addition circuit by testing every combination of 8 bit numbers and verifying the outputs match the goal values. I can't prove the same circuit by running 200 random additions and saying "none of these had errors, must be good", despite being extremely confident in it. The problem with a lot of actual math things is the search space is infinite (see the number of possible real coefficients in a quadratic function) unless you start doing smart things to limit the bounds of what you need to check, which comes back to logical theorem proving tactics. Sometimes a combination of these methods is used, e.g. the initial validations of the 4 color theorem, where you limit the search space to something reasonable but not prove it straight out then simply check the remaining cases. For a famous example, take Skewe's number. It's an upper bound for when the number of primes below x finally exceeds the logarithmic integral approximation of the same value but even the lower bound is ridiculously high. We have a logical proof the functions swap who is greater an infinite number of times but it'd be quite easy to run some test like this with floats and still conclude we've proven li(x) < pi(x). Heck, it's even possible the gaps in floats at that scale are large enough to just skip a crossover entirely.
- gosub100 3y ago
  thank you for the detailed answer :)

zamadatix 3y ago

The problem is we can't believe things like "we sampled the first 10^6 examples we came up with and it held so we can trust it to be valid". These are still just conjectures and sometimes turn out to be false at extreme bounds or corner cases. This doesn't mean conjectures (or even known sometimes-false approximations) are useless, it's just a different discussion vs what is trying to be done with these tools. One case you can get away with this is exhaustively checking the ENTIRE search space. E.g. I can prove an 8 bit addition circuit by testing every combination of 8 bit numbers and verifying the outputs match the goal values. I can't prove the same circuit by running 200 random additions and saying "none of these had errors, must be good", despite being extremely confident in it. The problem with a lot of actual math things is the search space is infinite (see the number of possible real coefficients in a quadratic function) unless you start doing smart things to limit the bounds of what you need to check, which comes back to logical theorem proving tactics. Sometimes a combination of these methods is used, e.g. the initial validations of the 4 color theorem, where you limit the search space to something reasonable but not prove it straight out then simply check the remaining cases. For a famous example, take Skewe's number. It's an upper bound for when the number of primes below x finally exceeds the logarithmic integral approximation of the same value but even the lower bound is ridiculously high. We have a logical proof the functions swap who is greater an infinite number of times but it'd be quite easy to run some test like this with floats and still conclude we've proven li(x) < pi(x). Heck, it's even possible the gaps in floats at that scale are large enough to just skip a crossover entirely.

gosub100 3y ago
thank you for the detailed answer :)