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?
> 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.
> 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.
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.
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.)
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.
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.
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).
> 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.
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?
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.
It seems there are a lot of different formalization systems. (11 listed on this site).
It seems strange to me that there isn't one standard system.
I don't know much about modern mathematics. But seems odd to me there isn't more of a movement to formalise all proofs. And to get computers / AI involved in discovering new proofs.
Please some explain to me!
(I have lots of ignorance of these things)
> It seems strange to me that there isn't one standard system.
It would be much stranger to me if there was only one.
These formal systems are much like programming languages, and just like those, come in many flavors, appealing to different appetites.
Where programming languages can be based on procedures, objects, or functions, proof systems can be based on set theory, on simple type theory, or on dependent type theory.
In his comparison of formal systems [1], Freek Wiedijk identifies no less than seven ways to represent mathematics.
> These formal systems are much like programming languages, and just like those, come in many flavors, appealing to different appetites.
and they all compile into the same fol/hol assembly (e.g. Isabelle translates its languages to fol and uses E for actual theorem proving, and E knows nothing about Isabelle language coolness), so in theory they should be able to integrate nicely.
My understanding is that the problem is they formalize in different mathematical foundations/axiomatic theories, but I am not an expert in this.
I meant to say they are all the same thing on logical level, all those fancy typed theories can be reduced to hol/fol, for some it is implemented, for others not.
Not an expert, but I think your question is roughly analogous to asking why there isn't one programming language.
There are many different approaches to writing formalization systems, and so far we don't have one that has won out as clearly superior (though from the outside it looks like Lean has the most momentum, and is the only one that has been used on cutting edge mathematics as far as I know).
On your question why there isn't more of a movement to formalize proofs: Proofs as written are for communicating and convincing other humans. Humans are _very_ good at filling in gaps. You can say things like: "In what follows we need this minor property to hold, it can be proven easily using Properties 4, 5, and 6 established above by using the strategy X". Here easily means "easy for a specialist who has dedicated 10 years to study this stuff", which is the target audience for your writing. If you instead need to explain this minor result to a formalization engine, you have to spell out every. single. last. detail.
The skills needed to formalize the proof and come up with the proof are probably quite distinct. There are many people now who understand the proof well. Also, even if Wiles would be the best person to do it, he might be more inclined to spend the next five years on new mathematical ideas rather than on convincing a computer program his old ideas are correct.
Theorem provers aren't just for mathematicians formalizing mathematics. Although, for that purpose, Lean seems to be very popular these days (perhaps followed by Coq?). Theorem provers are also used to formalize software and hardware systems. The people using theorem provers are diverse in their tasks and priorities.
Consider three provers/languages: Coq, ACL2, and Dafny.
Coq is a very expressive, dependently-typed, higher-order functional language, much in the spirit of Haskell or SML. It is very powerful for writing specifications due to this expressivity, and is therefore a compelling candidate for formalizing mathematics. It also has a very clean separation between proof search and proof checking, allowing for a smaller trusted kernel in the proof checker. However, due to the complexity of the language, writing proofs tends to be a largely manual task, or require domain-specific automation.
ACL2, on the other hand, is simpler in its language. It is a first order logic, built atop a total, untyped (at least logically) lisp. It does not produce proof artifacts like Coq, but proofs are much more automated, consisting of only a handful of hints instead of an entire tactic-tree.
Finally, Dafny is an imperative language, very much resembling popular and ubiquitous languages familiar to every programmer. Proofs are managed by adding inline annotations, specifying pre and postconditions, invariants, etc. This does not expose hardly any of the proof internals, and may be difficult for large proofs, but is a relatively friendly interface for the working software engineer.
> But seems odd to me there isn't more of a movement to formalise all proofs.
Well, from the perspective of mathematicians all known proofs are formalized by definition (to some extent anyway). Putting them through a proof checker is not completely without merit, but is not exactly highest priority.
As for discovering new proofs, it's a bit tricky to tell a computer what to find interesting. And the reasoning behind a proof is often more important than the exact steps themselves.
Nowadays, there is indeed a movement towards interoperability between the various proof assistants, one of these bridge-building projects is called Dedukti: https://deducteam.github.io/ It's a challenging project because the different proof assistants which are currently in use differ in their foundational perspectives and their idioms. The question how to best formalize mathematics is still an open research problem, just as the question how to best develop programs, but we already have quite a good understanding of many important issues in this area.
> I don't know much about modern mathematics. But seems odd to me there isn't more of a movement to formalise all proofs.
Only a tiny percentage of mathematicians use such systems. Historically they arose from CS, not math, so most mathematicians aren't trained in it. And until recently, the two camps spoke different languages (i.e. different terminology for the same concept), so there was a barrier for a given mathematician to learn, say, Coq.
It's also very time consuming. A proof a mathematician can write down in 10 minutes may take him a day to formalize in a proof assistant.
Still, things are changing, and more mathematicians are toying with them. You can see Terence Tao experimenting with Lean on his Mastodon account: https://mathstodon.xyz/@tao
I vaguely remember from my undergrad that formalising all proofs isn't possible, due to axiom of choice making some issues (and if you decide to abandon axiom of choice, like in constructive mathematics, you lose real numbers).
It was a very interesting class, we mostly used Coq.
1. In those proof assistants which don't have the axiom of choice built-in, you can still formalize proofs depending on this axiom by putting it as an extra assumption. One repository using this style which I particularly like is the one by Martín Escardó: https://www.cs.bham.ac.uk//~mhe/TypeTopology/index.html He even takes care to explicitly put axioms as visible assumptions which are almost always taken for granted, such as function extensionality.
2. You don't need the axiom of choice to construct the real numbers, in fact several constructions are available (Dedekind cuts, Cauchy sequences, Cauchy processes, ...) and all do their job. It's just that without the (countable) axiom of choice, you cannot prove that the Cauchy real numbers are complete. But the other constructions work fine even in the absence of choice.
Coq is constructive be default, but you can add the axiom of choice and the law of the excluded middle to make it classical (other common axioms are functional extensionality, propositional extensionality, and proof irrelevance).
Perhaps you are recalling Godel's incompleteness theorem, which says that for any finite formal system (like Coq) there exists a true theorem it is unable to prove?
I've seen the same reaction from people learning to program. Why are there thousands of programming languages? Why not put everything under one standard?
The main answer, as for many variations of this question (languages, laws, units of measure, programming languages), is history. Efforts to formalize mathematics have spawned in different universities, at different times, in different teams with different cultures and approaches. The mathematical theories underlying the software also vary greatly. There isn't one agreed upon formalization of mathematics. There's classical logic and there's intuitionistic logic, which wants to see every existence theorem backed by an actual witness and does not agree that `not (not A) = A`. (Speaking of which, different systems have (very) different notions of equality! In case you thought this one would at least be simple). Sometimes two pieces of software have nearly identical foundations, such as Lean and Coq to some extent; but one is decades old, and the other is a rewrite from scratch using other unification algorithms and a different programming language. Sometimes people just don't get along and start competing projects.
Note that some people have intended to unify various proof systems, which reminds me of the classical https://xkcd.com/927/
33. Fermat's Last Theorem
has yet to be proven in a formal system. It's like Formal's Last Theorem :-)