An automatic theorem proving project
gowers.wordpress.com
gowers.wordpress.com
I think the direction that is ripe for advance is a two-part process: (1) translating from human-language mathematics proof to computer-verifiable formal proof language combine with (2) GPT3-style automated generation of plausible next-steps in human language proofs.
Gowers emphasizes the success of humans at "pruning" to only consider potentially useful next steps in a proof. I think GPT3 demonstrates such pruning in generating plausible natural language text continuations.
And the success of natural language translation between natural languages suggests natural->formal language translation may also be ripe.
Combined with the success of formal language automated theorem provers, it seems plausible to build on current technologies a stack that produces formally verified natural language proofs.
An AI researcher would be trying to build a better prover.
Gowers is a mathematician looking for mathematical insight.
This project's success would be based on how well it answers those fundamental questions he posed (i.e How does a human generate proofs, given no algorithm exists to solve the halting problem?)
The output might be more like meta mathematics, with insights provided by software, rather than ML software optimised for a goal.
Understanding how ML models work is a notorious problem.
A classical algorithm can be formally understood better - I think it's this mathematical understanding Gowers is looking for.
"Hunch" is a label we use for "I don't know explicitly how I came up with this".
Generally, when we have a label for a concept the description of which starts with "I don't know...", some people try and follow up with questions: is that a thing it is possible, in principle, to know? How could we find out for certain? If it's knowable, how do we get to know what it is?
Sometimes, they succeed, and generations of such successes is how we end up with the modern world.
There's a lot to unpack in just this.
Can we define an algorithm to generate hunches? (mathematical intuition).
Given infinite hunches, can we define an algorithm to order hunches by priority, to search?
That's the kind of question they'll be thinking about using the symbolic logic/classical algorithms in GOFAI approaches.
To be fair, this has some trivial answers -- despite being a fascinating question.
For example, given a formal proof verification system (e.g. Lean), you can search for proofs (either by brute force or hopefully using heuristics) and if a proof exists, you will find it after some finite time. The problem is that sometimes no proof exists. You may be thinking of getting "smart", and also trying to prove no proof exists in parallel. But that's just another proof, such that this recursion tower (proof that (proof that (... proof doesn't exist)) doesn't resolve. But I think overall this mostly means you should be able to accept non-existence or arbitrary proving times of proofs (maybe also a sociological problem for mathematicians!). That's of course how human mathematics works: no one now if any famous theorem (e.g. Riemann hypothesis) will be proven within some time frame, or maybe never.
One mathematician often cannot "justify" their reasoning process to another if their thinking is even slightly different. For example what is intuitive for one side of the algebra/analysis divide is often not to people on the other side.
It is therefore unlikely that a human level computer program will think enough like humans that it can be justified to any human. And vice versa. For it to do so, it has to be better than the human, also have a model of how the human thinks, and then be able to break down thinking it arrived at one way to something that makes sense to the human.
If a computer succeeded in this endeavor, it would almost certainly come up with new principles of doing mathematics that would then have to be taught to humans to for humans to appreciate what it is doing. Something like this has already happened with Go, see https://escholarship.org/uc/item/6q05n7pz for example. Even so, humans are still unable to learn to play the game at the same level as the superhuman program. And the same would be true in mathematics.
This is more or less what Gowers is after. And that's exactly why he wants GOFAI instead of ML. He wants to understand how "doing mathematics" works?
Theorem provers starting from basic axioms are often looking for things that aren't in the esoteric weeds of a specific subfield as it often takes too long for them to generate a suitable set of theorems that establish those fields.
To be sure, this happened just two years after GPT-3. So 5 years for something which Gowers wants, but based on a large language model, seems in fact quite realistic.
>>doing some GAN like system of both generating problems that yet can’t be solved and a solver to solve them seems to obviate the need for human training data.
I don't see how this is supposed to work, what if the generator just outputs unsolvable problems?
Comparatively, it's even a hard problem to define anything resembling a board where the structure is fixed enough to apply something similar to positional evaluation to. What you want is a network that flags next steps in theorems as promising and allows you to effectively ignore most of the search space. If you have a good way to do this I think AlphaZero would be a promising approach.
But even if you get AlphaZero to work it doesn't solve the problem of understanding. AlphaZero made go players better by giving them more content to study but it didn't explicitly teach knowledge of the game. Strategically in Go, it's actually rather unsatisfying because it seems to win most of its games by entirely abandoning influence for territory and then relying on its superior reading skills to pick fights inside the influence where it often seems to win from what pro players would previously describe as a disadvantageous fight. This means the learnings are limited for players who have less good reading skills than AlphaZero as they can't fight nearly as well, which suggests abandoning the entire dominant strategy it uses.
My guess is that such a model would learn to compose a collection of lemmas that score as useful, produce sub-proofs for those, and then combine them into the final proof. This still mimics a sequence of plays closely enough that the scoring model could recognize "progress" toward the goal and predict complementary lemmas until a final solution is visible.
It may even work for very long proofs by letting it "play" a portion of its early lemmas which remain visible to the scorer but the proof sequence is chunked into as many pieces as the NLP needs to see it all and backtracking behind what was output is no longer possible. Once a lemma and its proof are complete it can be used or ignored in the future proof but modifying it sounds less useful.
I highly doubt you could get such a model to produce a useful collection of lemmas. Even if you could, I don't think a useful collection of lemmas progressing towards a goal has anywhere near the same structure as scoring a position in a game.
Ultimately for any AlphaZero technique to work you need a powerful position evaluation network. Almost all the magic happens in that network's pruning. It's quite remarkable that you can get a search of 80,000 nodes to do better that a search of 35,000,000 nodes. All of that is due to efficient pruning from the network. You haven't convinced me of any plausible approach to getting such a network here.
The problem with generating arbitrary math problems is that you can generate an infinite number of boring, pointless problems. For example, prove that there is a solution to the system of equations x + 2y + 135798230 > 2x + y + 123532 and x - y < 234. Training an AI system how to solve these problems doesn't do anything.
I think we are in a stage for mathematics similar to where solving Go was in the 80's. For Go back then we didn't even have the right logical structure of the algorithm, we hadn't invented Monte Carlo tree search yet. Once a good underlying structure was found, and we added on AI heuristics, then Go was solvable by AIs. For mathematics I think we also need multiple innovations to get there from here.
Consider that mathematics requires greater precision in that the language has more exacting meanings and fewer plausible alternatives. Also consider that the bar to doing something useful in mathematics is extremely high. We're not trying to GPT3 a plausible sentence now, we're trying to guide GPT3 to producing the complete works of shakespeare.
GPT3 demonstrates a kind of pruning for generating viable text in natural language continuations but I'd argue it is nothing like pruning useful next steps of a proof. The pruning in GPT3 works as a probability model and is derived from a good data set of human utterances. Generating a good dataset of plausible and implausible next steps in mathematical proofs is a much harder problem. The cost per instance is extremely high as all of the proofs have to be translated into a specific precise formal language (otherwise you explode the search space to be any plausible utterance in some form of English+Math Symbols making the problem much harder). Even worse, different theorem provers want to use different formal languages making the reusability of the data set less than typical in ML problems. The dataset is also far smaller. How many interesting proofs in mathematics are at a suitable depth from the initialization of a theorem prover with just some basic axioms? Even if you solve the dataset problem though there are further problems. GPT3 isn't designed to evaluate the interestingness of a sentence, only the plausibility with hopes that the context in which the sentence is generated provides enough relevance.
In short, I'm highly skeptical that benefits in natural language translation will translate to formal languages. I'd also argue the problems you classify into "formal language translation" aren't even translation problems.
I also think very few people see the technologies you've mentioned as related (for good reason) and I think a program that attempts to build on them is likely to fail.
> the bar to doing something useful in mathematics is extremely high
Ah but the bar to do something interesting in automated theorem proving is much lower. Solving exercises from an advanced undergraduate class involving proofs would already be of interest.
> Generating a good dataset of plausible and implausible next steps in mathematical proofs is a much harder problem.
There are thousands of textbooks, monographs, and research mathematical journals. There really is a gigantic corpus of natural language mathematical proofs to study.
In graduate school there were a bunch of homework proofs which the professors would describe as "follow your nose" : after you make an initial step in the right direction the remaining steps followed the kind of pattern that quickly becomes familiar. I think it is very plausible that a GPT3 style system trained on mathematical writing could learn these "follow your nose" patterns.
> problems you classify into "formal language translation" aren't even translation problems
Fair. Going from natural language proofs like from a textbook to a formal language like automatic theorem provers use has similarities to a natural language translation problem but it would be fair to say that this is its own category of problem.
I question whether you'd get high enough accuracy out of a pattern matching type model like GPT3 that occasionally chooses an unusual or unexpected word. Given how frequently translating A->B->A yields A* instead of A with GPT3 I wonder if we are actually successfully capturing the precise mathematical statements.
(The problem of tractability also comes up wrt. type systems in computer languages, and of course "modality" in logic has been usefully applied to both human language/cognition and commonly used PL constructs such as monads.)
So far, we’ve started publishing about shape types encoded that way and are hoping to get to Zn group models by the end of the year. (Work is done, but I’m a slow writer.)
https://www.zmgsabstract.com/whitepapers/shapes-have-operati...
Generally speaking, some proofs will be easy in those specific logics and other proofs will be hard or impossible. The problem won't be equivalent to reducing useful subsets of math to such logics however as you will often want to prove a lemma in one logic and a theorem in another. The fact that you don't have a good vehicle for dealing with the union of statements from each distinct fragmented logic makes the entire exercise fall apart.
Instead, most theorem provers need to operate in a single logic so that they can easily build on previous results.
Not sure why this would inherently be an issue, since one can use shallow embeddings to translate statements across logics, and even a "union" of statements might be easily expressed in a common logical framework. But perhaps I'm missing something about what you're claiming here.
I'm claiming the common logical framework won't have all the nice properties that come from the careful restriction in each of the individual logics.
Sure, but this kinda goes without saying. It nonetheless seems to be true that if you want to come up with "justified" proofs, you'll want to do that proving work in logics that are more restricted. You'll still be able to use statement A for a proof of B; what the restriction ultimately hinders is conflating elements of the proofs of A and B together, especially in a way that might be hard to "justify".
It's not a promising approach if the only statements of the prover you can justify are the simplest and most basic ones.
> However, while machine learning has made huge strides in many domains, it still has several areas of weakness that are very important when one is doing mathematics. Here are a few of them.
Basically all of these claims are wrong. I'm not saying we have maybe perfectly solved them but we have solved them all to a great extend and it currently looks like if just scaling up further probably solves them all.
> In general, tasks that involve reasoning in an essential way.
See Google PaLM. Or most of the other recent big language models.
> Learning to do one task and then using that ability to do another.
Has been done many times before. But you could also again count the big language models as they can do almost any task. Or the big multi-modal models. Or then the whole area of multi-task learning, transfer learning. This all works very well.
> Learning based on just a small number of examples.
Few-shot learning, zero-shot learning, meta learning allows to do just that.
> Common sense reasoning.
Again, see PaLM or the other big language models.
> Anything that involves genuine understanding (even if it may be hard to give a precise definition of what understanding is) as opposed to sophisticated mimicry.
And again, see the big LMs.
Sure, you can argue this is not genuine understanding. Or there is no real common sense reasoning in certain areas. Or whatever other shortcomings with current approaches.
I would argue, even human intelligence falls short by many of that measures. Or humans also do just "sophisticated mimicry".
Maybe you say the current models lack long-term memory. But we already also have solutions for that. Also see fast weights.
The argument that humans just use a small number of examples to learn ignores all the constant stream of data we passively get through our life through our eyes, ears, etc. And also the evolutionary selection which sets the hyper parameters and many wiring paths of our brains.
Reasoning is the same. Where can I find a language model that reads a phrase and explains what grammar rules it violates?
Aw, this sets off the alarm bells for me. My immediate reaction is that this guy has no clue what he is getting into, apart from his "domain experience" (ie. top level mathematician). Run for the hills, I say.
As for logic, I am sure Gowers knows about Gödel, Church and Turing, so that should not be a problem ...
Furthermore, your statement of Gödel's incompleteness result is wrong, as it directly contradicts Gödel's completeness result. It's not that you cannot prove all true statements for a non-trivial axiomatic formal system. But it is rather that your non-trivial axiomatic formal system does not mean what you might want it to mean as you will always have non-standard models alongside your intended standard model. So that's actually an argument FOR Gowers' approach, because it means that an automated mathematician needs to reach beyond formal logic and capture this elusive notion of intuition.
Gowers wants to understand how the typical mathematician comes up with a proof. How is the proof found? Where do the ideas come from?
To some extent, this is orthogonal to whether or not you do maths constructively. But since 99.9% of mathematicians have never heard of constructive mathematics, and just use AoC or LEM all over the place, I am quite certain that Gowers is very much interested in how to find proofs in the "ordinary" sense: including the use of AoC and LEM.
What if instead of a chain-of-proofs-of work, there would be a chain-of-proofs?
And, what if instead of a chain, it was a directed-acyclic-graph-of -proofs?
(From now on I will use the term blockgraph instead of blockchain to disambiguate.)
Lastly: instead of a giant Ponzi scheme of useless deflationary pretend money, what if the blockgraph was simply backed by real dollars used to reward useful proofs?
That last bit is the most important: What's a useful proof? Why would anyone pay money for such a thing? Why would anyone care about a not-a-blockchain that won't make anyone super rich?
I like to imagine a "superoptimising compiler" that has a $1K/annum license. That's peanuts to a FAANG or even a medium-to-large org with a development team. This money would go "into the blockgraph"[1], compensating the authors of the "most useful proofs of more optimal code sequences".
Obviously a lot of effort would have to go into designing the blockgraph to avoid it being gamed or abused, because it is a lot more complex than comparatively trivial proof-of-work linear chains like Bitcoin.
The idea is that each proof published to the blockgraph would be identified by its hash, and would build upon existing proofs in the chain by referencing their hash codes in turn. So each proof would be a series of terms, most of which would be cross-references, as well as some novel steps that are difficult to generate but trivial to verify.
To disincentivise users spamming true but useless proofs such as "1+1=2" and "2+2=4", the system would have to penalise proofs based on the data volume of their novel component plus some smaller penalty of the total number of references, plus an even smaller penalty for indirect (transitive) references.
Existing proofs that are referenced get a "cut" of the real money income granted to proofs that reference them. This makes single-use proofs worthless to publish, and widely usable proofs potentially hugely lucrative.
Publishing shortcuts in the proof graph are rewarded, because then other proofs can be made shorter in turn, making them more profitable than longer proofs.
Etc...
In general, the design goal of the whole system is to have a strong incentive to publish short, efficient proofs that reuse the existing blockgraph as much as possible and can in turn be reused by as many other users as possible. This makes the data volume small, and proofs efficient to verify.
The people putting up real money can get their "problems solved" automatically via a huge marketplace of various proofs systems[2] interacting and enhancing each other.
Want a short bit of code optimised to death? Put the "problem" up on the blockgraph for $5 and some system will try to automatically find the optimal sequence of assembly instructions that provably results in the same outcome but in less CPU time.
A compiler could even do this submission for you automatically. Feed in $1K of "optimisation coins" and have it put up $50 every time there's a major release planned.
Want to optimise factory production scheduling with fiendishly complex constraints? Put up $10K on the blockgraph! If it gets solved, it's solved. If not... you don't lose your money.
Etc...
[1] The obvious way to do this would be to link the blockgraph to an existing chain like Bitcoin or Ethereum, but it could also be simply a private company that pays out the rewards to ordinary bank accounts based on the current blockgraph status.
[2] Don't assume computers! This isn't about rooms full of GPUs burning coal to generate useless hash codes. A flesh and blood human could meaningfully and profitably contribute to the blockgraph. A particularly clever shortcut through the proof space could be worth millions, but would never be found by automated systems.
> To disincentivise users spamming true but useless proofs such as "1+1=2" and "2+2=4", the system would have to penalise proofs based on the data volume of their novel component
I believe that this stated goal of defining a metric that decides which theorems are "interesting" is a lot more difficult than finding proofs for theorems.
I think at some point proving things will to a large part be automatic, and mathematicians will mostly concern themselves with finding interesting theorems, definitions, and axioms, rather than wasting time on proving-labor.
But what do I know.
"Useful & short" however can be. Useful proofs are ones that solve the problems that are placed on the chain with real money rewards. The length/size of the proof is trivially verifiable. Useful AND short is the combination that's required. "Useful" alone would result in duplicate spam. Merely "short" would result in bulk generation of useless proofs. "Useful and short" means that the core of the graph would be optimised much like ants looking for food. Shorter AND useful paths to many goals are automatically rewarded. Longer paths can exist, but as they get more used, the incentive to try and optimise them rises dramatically to the point where even humans might want to contribute clever shortcuts manually.
> Proof of excellence
> One interesting, and largely unexplored, solution to the problem of [token] distribution specifically (there are reasons why it cannot be so easily used for mining) is using tasks that are socially useful but require original human-driven creative effort and talent. For example, one can come up with a "proof of proof" currency that rewards players for coming up with mathematical proofs of certain theorems
You'd just get paid, almost like freelance work. But it would be a public graph, the payments could be millions of micropayments tracked by the graph, etc...
I initially thought "why do we need another one of these", like rolling your eyes at another programming language or JS framework. There's even another large-scale research project already underway at Cambridge [3].
I thought this extract from Gower's longer manifesto [4] captured the problem they're trying to solve:
"(just consider statements of the form “this Turing machine halts”), and therefore that it cannot be solved by any algorithm. And yet human mathematicians have considerable success with solving pretty complicated looking instances of this problem. How can this be?"
The heart of this project is understanding this problem - not creating another proof formalisation language. To understand algorithms that can prune the search space to generate proofs, using a "Good Old Fashioned AI" (GOFAI) approach, rather than machine learning.
Gowers makes a point to contrast their GOFAI approach with ML - they're interested in producing mathematical insights, not black-box software.
[0] https://leanprover.github.io/
[2] https://isabelle.in.tum.de/
[3] https://www.cl.cam.ac.uk/~lp15/Grants/Alexandria/
[4] https://drive.google.com/file/d/1-FFa6nMVg18m1zPtoAQrFalwpx2...
I had a complete opposite reaction to yours. I feel like automatic proving languages are very quirky and stem from the creators not really knowing much about programming. At my university a bunch of professors who really liked Prolog made a formal proving language and guess what syntax it had? Yeah... terrible stuff.
Personally it's been a few years since I started thinking about this matter, but one of my personal objectives in live is to create a decently simple and intuitive (for both mathematicians and programmers) environment for formally proving their theorems
IMO, syntax is really not the main attraction, neither is it the main problem to solve when writing a theorem prover. Prolog has the advantage of a regular syntax, just like lisp.
Instead of wanting to make your miracle-own-thing, it would be far better to contribute to something like Idris. It's brilliant and in dire need of libraries.
Making formal proving simple and intuitive is the first step to have it heavily adopted. It should look as close as possible to writing a proof in pure first order logic.
I think there's room for a spectrum of theorem provers made for academic pure mathematicians, industry programmers and everything in between. Those should perhaps not have identical syntax, neither should they have the same goals.
To support my point, here's an example of an exotic theorem prover: https://github.com/webyrd/mediKanren It is aimed at medical researchers, and computes proofs about the medical literature, no less! This is a very different system and audience than which you are thinking about, but it's still a theorem prover.
In an analogy with traditional programming I'd say we have goto but we are yet to have structured loops. Enormously powerful but still hard to apply to either real mathematics or real problem.
But I have the impression Gowers dismisses the insights of what he calls machine-oriented ATP. These systems were --- perhaps are --- optimized on all levels of abstraction. From advances in the theory of which parts of the search space could be eliminated without loss of generality to optimizing the layout of c structs to improve cache locality.
But he's a mathematician, not an AI researcher - they have different goals.
Many AI researchers are interested in creating tools that solve problems (or proofs in this case).
Most mathematicians find proofs interesting for the insights they provide, not just the solution output.
You could say Gowers is looking for meta-proofs that provide insights on proof generation. It makes sense for him to emphasise the symbolic logic approach of GOFAI, here.
I would speculate Gowers is looking at higher-level abstractions that capture the essential semantics mathematicians are interested in - very much like a higher level programming language that humans understand.