6 ms·

Theorem proving is something I'm curious about. Can someone familiar explain why it's difficult, say, in an imperative language, to represent mathematical notat

Theorem proving is something I'm curious about. Can someone familiar explain why it's difficult, say, in an imperative language, to represent mathematical notation? I'm not saying its impossible, but why can't you start from 0 = 0, and apply random permutations with symbols on either side, check them for truth, discard the junk, and eventually arrive at the quadratic formula? Or a step further, derive (by randomly applying logical rules) the infinitely-many-primes theorem? Essentially, why can't you just trade CPU cycles for logical proofs and equations? What reading can you recommend that bridges (or addresses) programming language theory (BNF grammars, etc) to mathematics?

markusde 3y ago
A problem with randomly searching for theorems is that it blows up exponentially, and many of the theorems you would find are probably not useful in their own right. Another problem is that "check the for truth" is undecidable: they are what I think of when you mention "trade CPU cycles for proofs" though if you're just trying to prove random theorems they will be limited.
- jerf 3y ago
  "many of the theorems you would find are probably not useful in their own right" To give an example, there's an infinite array of "If X is greater than 20, X is greater than 10" theorems. Obviously useless to prove each of them, but enumeration will encounter all of these, as well as a huge number of classes of similar theorems, in the process of getting to anything interesting. You can't just "skip" them either, because they get arbitrarily complicated. I chose a really simple one to drive home the point, and because it's the sort of theorem you'll hit early, but tautologies can be arbitrarily complicated. Trying to create something that identifies them hits halting problems of their own. Rice's Theorem, which can be colloquially summarized as "any interesting property is not computable", will stop you, among other things. ("If X is a prime > 521, X does not have 21 as a factor." "If X is irrational, its fraction expansion does not have a denominator between 15 and 54." "If the absolute value of X is not equal to X, X < 932." "If the fractional component of X is greater than .5, the first digit of the fraction expansion is not 2 or 4." "The sum of two positive numbers is greater than the smallest of the two numbers number minus 273,883,192,823." "Most" theorems are really, really useless.)
  - someplaceguy 3y ago
    > "If X is greater than 10, X is greater than 20" theorems I think you meant in the opposite order, i.e.: "If X is greater than 20, then X is greater than 10" :) But otherwise your point is valid.
    - jerf 3y ago
      Whoops, yes, thanks, fixed. One of those things I edited one too many times and didn't catch in the end.
    - Koshkin 3y ago
      > > "If X is greater than 10, X is greater than 20" theorems I think I have seen theorems of that sort. (Can't think of a specific example right now.)
      - someplaceguy 3y ago
        A theorem like that isn't provable (unless you're using some kind of nonstandard arithmetic). You could only prove it if you add something else, e.g. a precondition saying that X = 30.
        Koshkin 3y ago
        Right, if it can be asserted based on some independent assumptions that a positive X must be at least 30, then from those assumptions and X > 10 it would follow that X > 20.
        carnitine 3y ago
        It also just follows from X being >= 30.
  - gosub100 3y ago
    What if you narrowed down one side, like "Find a formula for solving arbitrary polynomial equations"? (I know this has been proven to not exist using human brainpower). but the idea would be: "I'm looking for a func that produces zeros to an input equation, now generate billions of tokens and evaluate them and keep the ones that minimize the search criterion". Couldn't that eventually find a useful result (for actually-solvable search spaces)? I can see how it would fall apart quickly for something like the Riemann Hypothesis, because you're searching not for an equation (well, if you found a counterexample, sure) but for a nebulous classification problem: all solutions to this equation ( this series of tokens from this language that return zero) must lie on (I can't recall if it was literally on, or "around") re(1/2). Once you try to reason with infinite sets (domain/codomain) the logic of a CPU can't help you nearly as much.
- Pet_Ant 3y ago
  Randomly searching for theorems is like using monkeys with typewriters to search for a lost work of Shakespeare. Sure, you _might_ find it, but you'd never know amongst the noise. Well, it wouldn't be like monkeys with typewriters, more like monkeys with word processors and grammar check because the results will type check... but there is no way to screen out what is interesting.
  - gosub100 3y ago
    I agree with monkeys+typewriters, but look at how compact the quadratic formula is. It's not a work of shakespeare. it's maybe 12 to 20 "tokens" , using a loose definition of a token. To me, it's totally within the realm of a 1-10 billion search space, isn't it? I'm just thinking aloud, but suppose a random-math-syntax shuffler eventually produced the quadratic formula, how would you even check it? You would have to input many permutations of quadratic equation inputs and check them against the randomly-produced one. You'd quickly hit imaginary numbers, which could (falsely) signal that the QF is invalid. Compare that to monkey-typing fizzbuzz. That seemingly could be done in a few billion iterations, no? (assume you could exclude monkeys from typing syntax errors, and only produce valid C++/java whatever). IDK, I'm just mesmerized by the fact that the QF is so compact, yet there isn't an easily-discoverable way to derive it by brute force. (and I'm deliberately excluding AI because of how tiring the questions of the form "why can't AI do _____" are. I don't care that much about AI).
    - Pet_Ant 3y ago
      The Pythagorean theorem is even more compact, and even more impactful. But the low hanging fruit has been already picked for centuries and how would you detect a meaningful formula if you were give a 10GB text file of various ones?
    - tromp 3y ago
      > To me, it's totally within the realm of a 1-10 billion search space, isn't it? A proof of the theorem is going to be at least a few hundred bits, which is totally out of reach of brute force search. A 10 billion search space only covers 34 bits (less than 5 ASCII symbols) in which you'll struggle to even state the theorem.
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).
slaymaker1907 3y ago
> check them for truth This is extraordinarily difficult and sometimes impossible. Even first order logic is undecidable with regard to checking if a formula is decidable. That said, LEAN does leverage a SAT solver to try and do a bit of what you describe.

markusde 3y ago

A problem with randomly searching for theorems is that it blows up exponentially, and many of the theorems you would find are probably not useful in their own right. Another problem is that "check the for truth" is undecidable: they are what I think of when you mention "trade CPU cycles for proofs" though if you're just trying to prove random theorems they will be limited.

jerf 3y ago
"many of the theorems you would find are probably not useful in their own right" To give an example, there's an infinite array of "If X is greater than 20, X is greater than 10" theorems. Obviously useless to prove each of them, but enumeration will encounter all of these, as well as a huge number of classes of similar theorems, in the process of getting to anything interesting. You can't just "skip" them either, because they get arbitrarily complicated. I chose a really simple one to drive home the point, and because it's the sort of theorem you'll hit early, but tautologies can be arbitrarily complicated. Trying to create something that identifies them hits halting problems of their own. Rice's Theorem, which can be colloquially summarized as "any interesting property is not computable", will stop you, among other things. ("If X is a prime > 521, X does not have 21 as a factor." "If X is irrational, its fraction expansion does not have a denominator between 15 and 54." "If the absolute value of X is not equal to X, X < 932." "If the fractional component of X is greater than .5, the first digit of the fraction expansion is not 2 or 4." "The sum of two positive numbers is greater than the smallest of the two numbers number minus 273,883,192,823." "Most" theorems are really, really useless.)
- someplaceguy 3y ago
  > "If X is greater than 10, X is greater than 20" theorems I think you meant in the opposite order, i.e.: "If X is greater than 20, then X is greater than 10" :) But otherwise your point is valid.
  - jerf 3y ago
    Whoops, yes, thanks, fixed. One of those things I edited one too many times and didn't catch in the end.
  - Koshkin 3y ago
    > > "If X is greater than 10, X is greater than 20" theorems I think I have seen theorems of that sort. (Can't think of a specific example right now.)
    - someplaceguy 3y ago
      A theorem like that isn't provable (unless you're using some kind of nonstandard arithmetic). You could only prove it if you add something else, e.g. a precondition saying that X = 30.
      - Koshkin 3y ago
        Right, if it can be asserted based on some independent assumptions that a positive X must be at least 30, then from those assumptions and X > 10 it would follow that X > 20.
        carnitine 3y ago
        It also just follows from X being >= 30.
- gosub100 3y ago
  What if you narrowed down one side, like "Find a formula for solving arbitrary polynomial equations"? (I know this has been proven to not exist using human brainpower). but the idea would be: "I'm looking for a func that produces zeros to an input equation, now generate billions of tokens and evaluate them and keep the ones that minimize the search criterion". Couldn't that eventually find a useful result (for actually-solvable search spaces)? I can see how it would fall apart quickly for something like the Riemann Hypothesis, because you're searching not for an equation (well, if you found a counterexample, sure) but for a nebulous classification problem: all solutions to this equation ( this series of tokens from this language that return zero) must lie on (I can't recall if it was literally on, or "around") re(1/2). Once you try to reason with infinite sets (domain/codomain) the logic of a CPU can't help you nearly as much.
Pet_Ant 3y ago
Randomly searching for theorems is like using monkeys with typewriters to search for a lost work of Shakespeare. Sure, you _might_ find it, but you'd never know amongst the noise. Well, it wouldn't be like monkeys with typewriters, more like monkeys with word processors and grammar check because the results will type check... but there is no way to screen out what is interesting.
- gosub100 3y ago
  I agree with monkeys+typewriters, but look at how compact the quadratic formula is. It's not a work of shakespeare. it's maybe 12 to 20 "tokens" , using a loose definition of a token. To me, it's totally within the realm of a 1-10 billion search space, isn't it? I'm just thinking aloud, but suppose a random-math-syntax shuffler eventually produced the quadratic formula, how would you even check it? You would have to input many permutations of quadratic equation inputs and check them against the randomly-produced one. You'd quickly hit imaginary numbers, which could (falsely) signal that the QF is invalid. Compare that to monkey-typing fizzbuzz. That seemingly could be done in a few billion iterations, no? (assume you could exclude monkeys from typing syntax errors, and only produce valid C++/java whatever). IDK, I'm just mesmerized by the fact that the QF is so compact, yet there isn't an easily-discoverable way to derive it by brute force. (and I'm deliberately excluding AI because of how tiring the questions of the form "why can't AI do _____" are. I don't care that much about AI).
  - Pet_Ant 3y ago
    The Pythagorean theorem is even more compact, and even more impactful. But the low hanging fruit has been already picked for centuries and how would you detect a meaningful formula if you were give a 10GB text file of various ones?
  - tromp 3y ago
    > To me, it's totally within the realm of a 1-10 billion search space, isn't it? A proof of the theorem is going to be at least a few hundred bits, which is totally out of reach of brute force search. A 10 billion search space only covers 34 bits (less than 5 ASCII symbols) in which you'll struggle to even state the theorem.

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

slaymaker1907 3y ago

> check them for truth This is extraordinarily difficult and sometimes impossible. Even first order logic is undecidable with regard to checking if a formula is decidable. That said, LEAN does leverage a SAT solver to try and do a bit of what you describe.