3 ms·

> Can someone familiar explain why it's difficult, say, in an imperative language, to represent mathematical notation? Is the question whether you can represen

by xavxav 3y ago

> Can someone familiar explain why it's difficult, say, in an imperative language, to represent mathematical notation? Is the question whether you can represent mathematical notation in an imperative language, or whether you can search for mathematical proofs in an imperative language? Or is it a broader question about why theorem provers usually use functional languages? 1. Representing mathematical notation is not any harder in an imperative language than a functional one: it's just an AST. Syntax isn't the hard part however, it's semantics which are tricky. For example, you say "apply random permutations with symbols on either side, check them for truth", but "checking for truth" isn't automatically possible. What if I randomly generated "P = NP", is that true? 2. You can totally write search procedures in an imperative language, generally these programs are earlier than in a functional language, but again there's nothing fundamental about the language choice here. SMT solvers are an example of this. 3. You may notice that many theorem provers incorporate a functional language as 'the language of proofs'. This is due to the 'Curry-Howard Isomorphism', which in short establishes a correspondence between theorems and types, and programs and proofs. For example, I could ask you "does there exist a function from A to A" and you could answer "yes, it's the identity function". You've just proved that there exists an item of type "A -> A". However, this correspondence stops making sense if functions can diverge or have side-effects. You also typically want higher-order closures and pattern matching, and at that point, you've got a functional language.

gosub100 3y ago
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 :)
BeetleB 3y ago
> Representing mathematical notation is not any harder in an imperative language than a functional one: it's just an AST. Not quite - it's a bit trickier. Common mathematical notation used by mathematicians is not formal, as you often hear people on HN complain about. The same expression means different things in different contexts, and even those contexts are not easy to extract formally. ab could mean the multiplication of two variables, or something else, and occasionally you'll see both uses in the same section/proof. Mathematicians don't want to be formal to the level that computers require. It'll really slow them down.
- mikhailfranco 3y ago
  Physicists don't want to be formal to the level that mathematicians require. It'll really slow them down. Chemists ... (xkcd)

by xavxav 3y ago

gosub100 3y ago

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 :)

BeetleB 3y ago

> Representing mathematical notation is not any harder in an imperative language than a functional one: it's just an AST. Not quite - it's a bit trickier. Common mathematical notation used by mathematicians is not formal, as you often hear people on HN complain about. The same expression means different things in different contexts, and even those contexts are not easy to extract formally. ab could mean the multiplication of two variables, or something else, and occasionally you'll see both uses in the same section/proof. Mathematicians don't want to be formal to the level that computers require. It'll really slow them down.

mikhailfranco 3y ago
Physicists don't want to be formal to the level that mathematicians require. It'll really slow them down. Chemists ... (xkcd)