Hacker News Reader

Comment by gosub100 | Hacker News Reader

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?

View on HN

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

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

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.

thank you for the detailed answer :)

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

Physicists don't want to be formal to the level that mathematicians require. It'll really slow them down.

Chemists ... (xkcd)

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.

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

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

Whoops, yes, thanks, fixed. One of those things I edited one too many times and didn't catch in the end.

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

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.

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.

It also just follows from X being >= 30.

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.

Simply generating all possible tokens is already an exponential problem. There really isn't any way around that. Analysis of them for any interesting property becomes super-exponential pretty easily.

If you are going to do something more clever than "generate all tokens", then you're no longer talking about the same thing, and the analysis depends on the nature of your "more clever". Although starting with an exponential (or super exponential) process and then trying to "cut it down" to something reasonable is almost always a fool's errand anyhow. Starting yourself out in the position where you are not only behind the eight ball but have essentially already been murdered by it, and then cleverly working yourself back into a position where you've somehow won, is rarely, if ever, a good approach to solving a problem.

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.

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

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?

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

> 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?

Even 12 tokens with only 10 different token values gives you 10¹² different candidate ‘proofs’. That already is a thousand times 10 billion.

In reality, there easily are 100 possible token values (lower and upper case alphabet, punctuation, Greek lower and upper case, dozens of symbols, a bit of Hebrew, etc), taking that number to 10²⁴.

Also, I think even just express the two solutions to ax²+bx+c=0 without any hint of a proof in twelve tokens is an insurmountable challenge.

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

Reply on news.ycombinator.com