5 ms·

Interesting, most theorem provers like lean [1], coq [2] and Isabelle [2] are concerned with formalization, and interactive theorem proving. I initially thoug

by yaseer 4y 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 4y 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 4y 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 4y 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 4y 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__ 4y 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 4y 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 4y 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 4y 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 4y ago
      That doesn't mean it is a proof that human have the slightest chance of understanding. It gets out of hand quickly.
      - yaseer 4y 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.

by yaseer 4y ago

HidyBush 4y 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 4y 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 4y 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 4y 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__ 4y 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 4y 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 4y 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 4y 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 4y ago
    That doesn't mean it is a proof that human have the slightest chance of understanding. It gets out of hand quickly.
    - yaseer 4y 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.