7 ms·

An automatic theorem proving project

163 points by ColinWright 5y ago

yaseer 5y ago
Interesting, most theorem provers like lean [1], coq [2] and Isabelle [2] are concerned with formalization, and interactive theorem proving. 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/ https://leanprover.github.io/ [1] https://coq.inria.fr/ https://coq.inria.fr/ [2] https://isabelle.in.tum.de/ https://isabelle.in.tum.de/ [3] https://www.cl.cam.ac.uk/~lp15/Grants/Alexandria/ https://www.cl.cam.ac.uk/~lp15/Grants/Alexandria/ [4] https://drive.google.com/file/d/1-FFa6nMVg18m1zPtoAQrFalwpx2YaGK4/view?usp=sharing https://drive.google.com/file/d/1-FFa6nMVg18m1zPtoAQrFalwpx2...
- HidyBush 5y ago
  >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 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
  - rscho 5y ago
    Are you implying that giving prolog-like syntax to a language suggests ignorance about programming? Why would that be terrible? 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.
    - HidyBush 5y ago
      Who are automatic theorem provers aimed at? Computer scientists with an interest in maths or mathematicians with an interest in CS? If you are a mathematician starting off with something like Coq is a nightmare. Nobody learns OCamel in college, math majors usually learn R, Python and maybe Java or C. 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.
      - rscho 5y ago
        IMO, you overstate the issue of syntax. As a hobbyist in both programming and math, Coq's syntax has never been the reason I failed to complete a proof. But perhaps I'm just too dumb and my difficulties lie elsewhere, so that's just my 2c. 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 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.
    - mhh__ 5y ago
      It's not really the syntax but rather that until very recently theorem provers have been quite niche even in formal disciplines, so the tooling isn't quite there. 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.
- funcDropShadow 5y ago
  > Gowers makes a point to contrast their GOFAI approach with ML - they're interested in insights, not black-boxes 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.
  - yaseer 5y ago
    I agree he seems quite disinterested in 'machine-oriented ATP'. 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.
    - funcDropShadow 5y ago
      But machine-oriented ATP is based on a symbolic-representation of formulas and terms. And the output is a proof formulated in the underlying logical calculus not just yes or no.
      - deadbeef57 5y ago
        That doesn't mean it is a proof that human have the slightest chance of understanding. It gets out of hand quickly.
        yaseer 5y ago
        Exactly - machine-formulated ATP often ends up like machine-code, very similar to the proofs of Russell's Principia Mathematica. Extremely low-level formalisms great for procedural reasoning, but poor for human understanding. 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.
dzdt 5y ago
This is the opposite direction to what I expected to see for new theorem proving efforts: "Good old fashioned AI" vs leveraging advances of deep learning for natural language. 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.
- ImprobableTruth 5y ago
  Human-language proofs for anything non-trivial are really just proof sketches, that's why you can't really meaningfully separate this into a two step process.
- yaseer 5y ago
  I don't think Gowers is trying to build a better theorem prover. 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.
  - amelius 5y ago
    They can still use ML to prune the search space, I suppose?
    - yaseer 5y ago
      For a mathematician, it's not the output of pruning the search space, but understanding how the search space is pruned. 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.
jiggawatts 5y ago
I apologise ahead for posting something in response to this which is technically off topic, and unfortunately also mentions blockchains. The comment by 'yaseer' reminded me of a vaguely related idea, so I figured some people reading this might be interested... 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.
zozbot234 5y ago
My hunch is that building "justified" proofs that avoid computer-driven brute force search ought to be the same as building proofs in a logic where finding a proof is computationally easy. We know that such logics exist (e.g. the multi-modal logics that have been proposed for use in the semantic web have been specifically chosen for computational tractability; in practice, multi-modal logic can also be viewed as a subset of FOL.). If so the problem is roughly equivalent to reducing useful subsets of math to such logics. (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.)
- zmgsabst 5y ago
  You can also convert your logic model into something that can be viewed as an image completion problem, eg, by translating categorical diagrams into a adjacency matrix and “completing” a partial one. (Hopefully, but preliminary results are encouraging.) 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-operations https://www.zmgsabstract.com/whitepapers/shapes-have-operati...
  - zozbot234 5y ago
    Very interesting work. Visual and diagrammatic reasoning are part of this problem, yes. It might turn out that some proofs that might be generally thought of as hard are actually "visually" justified, in a way that could even perhaps increase our power to justify mathematical statements. The extended paper Gowers links in his blogpost discusses one such case in depth, namely the well-known problem of whether a chessboard with two opposite corners removed can be tiled by two-square dominoes.
- TimPC 5y ago
  I've worked with logics where finding proofs are computationally easy and even logics where expensive steps can be explicitly bound and controlled for. I'm always very skeptical about claims that assert "the same". 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.
woopwoop 5y ago
For context for those outside of mathematics, Gowers is a preeminent mathematician who won a fields medal for his work in functional analysis. He has advocated and worked towards computer-generated mathematics for a long time, mostly along approaches roughly in line with this one. In particular, his interest in this topic predates the deep learning revolution (which I'll say began with alexnet, but wherever you date it the claim holds).
adamnemecek 5y ago
I wonder if this will be constructivist.
- deadbeef57 5y ago
  Here's my guess. 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.
- auggierose 5y ago
  No, it won't be.
smaddox 5y ago
Are we really sure that humans aren't brute force searching for proofs, through a combination of subconscious processing and network effects (i.e. many people working on the same problem and only some of them happen on to the correct path)?
- zozbot234 5y ago
  Gowers seems to be arguing that brute-force-searching for proofs at the highest levels of abstraction might be okay, so long as the proofs themselves don't use brute force, even indirectly. (This means that a proof step such as: "pick n=42 and the proof goes through. QED." would somehow have to be disallowed.)
albertzeyer 5y ago
It sounds as if the author is not well informed about the recent advancements and findings from the literature and research community on deep learning. > 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.
- zozbot234 5y ago
  Language models can only parrot back their training input. There's no generality to them at all; the best they can do is some crude, approximate interpolation of their training examples that may or may not be "correct" in any given instance. There are things that the typical AI/ML approach might be genuinely useful for (e.g. generating "probable" conjectures by leveraging the "logical uncertainty" of very weak and thus tractable logics) but mainstream language learning is a complete non-starter for this stuff.
robinzfc 5y ago
I think it is interesting to compare this to the previous attempt from 2013 by Gowers (and Mohan Ganesalingam) described in a blog series ending with https://gowers.wordpress.com/2013/04/14/answers-results-of-polls-and-a-brief-description-of-the-program/ https://gowers.wordpress.com/2013/04/14/answers-results-of-p... .
- zozbot234 5y ago
  Discussed https://news.ycombinator.com/item?id=5507176 https://news.ycombinator.com/item?id=5507176
waynecochran 5y ago
There was a ton of work on this in the 20th century, but the manifesto lacks a bibliography. How will this succeed where all the other brilliant folks from the past fell short?
- auggierose 5y ago
  To be harsh, one could probably argue that no one as brilliant as Gowers, and with his expertise in the domain, has worked on this in the past.
  - waynecochran 5y ago
    I have not heard of Gowers, but I have heard of Gödel, Turing, and Church. In fact, Gödel showed for any non-trivial axiomatic system there are true statements which cannot be proved in the system. So there is that.
    - auggierose 5y ago
      Well, none of those have worked on automated theorem proving. So there is that. 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.
mathgenius 5y ago
> (I myself am not a fluent programmer — I have some experience of Haskell and Python and I think a pretty good feel for how to specify an algorithm in a way that makes it implementable by somebody who is a quick coder, and in my collaborations so far have relied on my collaborators to do the coding.) 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.
- trenchgun 5y ago
  This is not his first rodeo. https://arxiv.org/pdf/1309.4501.pdf https://arxiv.org/pdf/1309.4501.pdf
lorepieri 5y ago
Related: https://math.stackexchange.com/questions/4438278/why-are-many-proofs-difficult-in-general/4438668#4438668 https://math.stackexchange.com/questions/4438278/why-are-man...
netmonk 5y ago
Rewriting COQ in Rust?

163 points by ColinWright 5y ago

Interesting, most theorem provers like lean [1], coq [2] and Isabelle [2] are concerned with formalization, and interactive theorem proving. 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/ https://leanprover.github.io/ [1] https://coq.inria.fr/ https://coq.inria.fr/ [2] https://isabelle.in.tum.de/ https://isabelle.in.tum.de/ [3] https://www.cl.cam.ac.uk/~lp15/Grants/Alexandria/ https://www.cl.cam.ac.uk/~lp15/Grants/Alexandria/ [4] https://drive.google.com/file/d/1-FFa6nMVg18m1zPtoAQrFalwpx2YaGK4/view?usp=sharing https://drive.google.com/file/d/1-FFa6nMVg18m1zPtoAQrFalwpx2...

HidyBush 5y ago
>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 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
- rscho 5y ago
  Are you implying that giving prolog-like syntax to a language suggests ignorance about programming? Why would that be terrible? 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.
  - HidyBush 5y ago
    Who are automatic theorem provers aimed at? Computer scientists with an interest in maths or mathematicians with an interest in CS? If you are a mathematician starting off with something like Coq is a nightmare. Nobody learns OCamel in college, math majors usually learn R, Python and maybe Java or C. 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.
    - rscho 5y ago
      IMO, you overstate the issue of syntax. As a hobbyist in both programming and math, Coq's syntax has never been the reason I failed to complete a proof. But perhaps I'm just too dumb and my difficulties lie elsewhere, so that's just my 2c. 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 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.
  - mhh__ 5y ago
    It's not really the syntax but rather that until very recently theorem provers have been quite niche even in formal disciplines, so the tooling isn't quite there. 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.
funcDropShadow 5y ago
> Gowers makes a point to contrast their GOFAI approach with ML - they're interested in insights, not black-boxes 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.
- yaseer 5y ago
  I agree he seems quite disinterested in 'machine-oriented ATP'. 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.
  - funcDropShadow 5y ago
    But machine-oriented ATP is based on a symbolic-representation of formulas and terms. And the output is a proof formulated in the underlying logical calculus not just yes or no.
    - deadbeef57 5y ago
      That doesn't mean it is a proof that human have the slightest chance of understanding. It gets out of hand quickly.
      - yaseer 5y ago
        Exactly - machine-formulated ATP often ends up like machine-code, very similar to the proofs of Russell's Principia Mathematica. Extremely low-level formalisms great for procedural reasoning, but poor for human understanding. 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.

dzdt 5y ago

This is the opposite direction to what I expected to see for new theorem proving efforts: "Good old fashioned AI" vs leveraging advances of deep learning for natural language. 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.

ImprobableTruth 5y ago
Human-language proofs for anything non-trivial are really just proof sketches, that's why you can't really meaningfully separate this into a two step process.
yaseer 5y ago
I don't think Gowers is trying to build a better theorem prover. 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.
- amelius 5y ago
  They can still use ML to prune the search space, I suppose?
  - yaseer 5y ago
    For a mathematician, it's not the output of pruning the search space, but understanding how the search space is pruned. 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.

jiggawatts 5y ago

I apologise ahead for posting something in response to this which is technically off topic, and unfortunately also mentions blockchains. The comment by 'yaseer' reminded me of a vaguely related idea, so I figured some people reading this might be interested... 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.

zozbot234 5y ago

My hunch is that building "justified" proofs that avoid computer-driven brute force search ought to be the same as building proofs in a logic where finding a proof is computationally easy. We know that such logics exist (e.g. the multi-modal logics that have been proposed for use in the semantic web have been specifically chosen for computational tractability; in practice, multi-modal logic can also be viewed as a subset of FOL.). If so the problem is roughly equivalent to reducing useful subsets of math to such logics. (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.)

zmgsabst 5y ago
You can also convert your logic model into something that can be viewed as an image completion problem, eg, by translating categorical diagrams into a adjacency matrix and “completing” a partial one. (Hopefully, but preliminary results are encouraging.) 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-operations https://www.zmgsabstract.com/whitepapers/shapes-have-operati...
- zozbot234 5y ago
  Very interesting work. Visual and diagrammatic reasoning are part of this problem, yes. It might turn out that some proofs that might be generally thought of as hard are actually "visually" justified, in a way that could even perhaps increase our power to justify mathematical statements. The extended paper Gowers links in his blogpost discusses one such case in depth, namely the well-known problem of whether a chessboard with two opposite corners removed can be tiled by two-square dominoes.
TimPC 5y ago
I've worked with logics where finding proofs are computationally easy and even logics where expensive steps can be explicitly bound and controlled for. I'm always very skeptical about claims that assert "the same". 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.

woopwoop 5y ago

For context for those outside of mathematics, Gowers is a preeminent mathematician who won a fields medal for his work in functional analysis. He has advocated and worked towards computer-generated mathematics for a long time, mostly along approaches roughly in line with this one. In particular, his interest in this topic predates the deep learning revolution (which I'll say began with alexnet, but wherever you date it the claim holds).

adamnemecek 5y ago

I wonder if this will be constructivist.

deadbeef57 5y ago
Here's my guess. 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.
auggierose 5y ago
No, it won't be.

smaddox 5y ago

Are we really sure that humans aren't brute force searching for proofs, through a combination of subconscious processing and network effects (i.e. many people working on the same problem and only some of them happen on to the correct path)?

zozbot234 5y ago
Gowers seems to be arguing that brute-force-searching for proofs at the highest levels of abstraction might be okay, so long as the proofs themselves don't use brute force, even indirectly. (This means that a proof step such as: "pick n=42 and the proof goes through. QED." would somehow have to be disallowed.)

albertzeyer 5y ago

It sounds as if the author is not well informed about the recent advancements and findings from the literature and research community on deep learning. > 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.

zozbot234 5y ago
Language models can only parrot back their training input. There's no generality to them at all; the best they can do is some crude, approximate interpolation of their training examples that may or may not be "correct" in any given instance. There are things that the typical AI/ML approach might be genuinely useful for (e.g. generating "probable" conjectures by leveraging the "logical uncertainty" of very weak and thus tractable logics) but mainstream language learning is a complete non-starter for this stuff.

robinzfc 5y ago

I think it is interesting to compare this to the previous attempt from 2013 by Gowers (and Mohan Ganesalingam) described in a blog series ending with https://gowers.wordpress.com/2013/04/14/answers-results-of-polls-and-a-brief-description-of-the-program/ https://gowers.wordpress.com/2013/04/14/answers-results-of-p... .

zozbot234 5y ago
Discussed https://news.ycombinator.com/item?id=5507176 https://news.ycombinator.com/item?id=5507176

waynecochran 5y ago

There was a ton of work on this in the 20th century, but the manifesto lacks a bibliography. How will this succeed where all the other brilliant folks from the past fell short?

auggierose 5y ago
To be harsh, one could probably argue that no one as brilliant as Gowers, and with his expertise in the domain, has worked on this in the past.
- waynecochran 5y ago
  I have not heard of Gowers, but I have heard of Gödel, Turing, and Church. In fact, Gödel showed for any non-trivial axiomatic system there are true statements which cannot be proved in the system. So there is that.
  - auggierose 5y ago
    Well, none of those have worked on automated theorem proving. So there is that. 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.

mathgenius 5y ago

> (I myself am not a fluent programmer — I have some experience of Haskell and Python and I think a pretty good feel for how to specify an algorithm in a way that makes it implementable by somebody who is a quick coder, and in my collaborations so far have relied on my collaborators to do the coding.) 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.

trenchgun 5y ago
This is not his first rodeo. https://arxiv.org/pdf/1309.4501.pdf https://arxiv.org/pdf/1309.4501.pdf

lorepieri 5y ago

Related: https://math.stackexchange.com/questions/4438278/why-are-many-proofs-difficult-in-general/4438668#4438668 https://math.stackexchange.com/questions/4438278/why-are-man...

netmonk 5y ago

Rewriting COQ in Rust?