4 ms·

If you've ever tried encoding proofs in a proof assistant such as Coq (which is what the INRIA folks used to encode the four color theorem and the Fiet-Thompson

by bollu 8y ago

If you've ever tried encoding proofs in a proof assistant such as Coq (which is what the INRIA folks used to encode the four color theorem and the Fiet-Thompson theorem), you'll realise just how painful it is --- I speak as someone who's done this for fun (and now for research. [my report is available here](https://github.com/bollu/dependence-analysis-coq/blob/master/report-independent-study/independent-study.pdf) https://github.com/bollu/dependence-analysis-coq/blob/master...)

noisem4ker 8y ago
https://github.com/bollu/dependence-analysis-coq/blob/master/report-independent-study/independent-study.pdf https://github.com/bollu/dependence-analysis-coq/blob/master... Put a space before the final ), else it becomes part of the URL. Thanks for the paper, by the way.
WalterGR 8y ago
If you've ever tried encoding proofs in a proof assistant such as Coq... you'll realise just how painful it is Is that a result of how painful the tool is to use? (And by “tool” I mean any such tool - coq or whatever.) What would need to be improved in the state-of-the-art of automated proof validation for the process to be less painful?
- patrickthebold 8y ago
  Imagine convincing someone that a web service could be written, vs getting it written and deployed to production. And none of its dependencies actually exist either. Like someone just said... relational database? Yeah we could write one of those...
- darkmighty 8y ago
  > What would need to be improved in the state-of-the-art of automated proof validation for the process to be less painful? I think there are two parts: 1) Improve the theorem proving languages syntax so it's more intuitive, and so there is a wealth of "libraries" to build upon so you don't have to go from the basic axioms (of arithmetic or the reals for example) any time you wanted to prove something. 2) Provide some sort of computational intelligence to fill in natural gaps of proofs. I believe humans tend to leave a large number of more or less trivial gaps even in rigorous mathematical proofs that couldn't be avoided by language syntax. For this probably some kind of AI system would be ideal that tries to derive successive results and complete the proof automatically.
  - AstralStorm 8y ago
    Isabelle semi-automatic theorem prover tries to help with 2 if you use sledgehammer strategy and print out the simplified proof with isar_proofs argument, which you can more easily read and reintegrate into the main document if needed. You can help its heuristics by providing it a set of potential proof facts explicitly. The libraries available for it are already quite huge... sometimes in a few encodings as well. (valued, typed, functional etc.) https://www.isa-afp.org/ https://www.isa-afp.org/
  - anonlastname 8y ago
    I think coq has some kind of ml software. I saw it mentioned in the proof general UI. I'm not sure how good it is
    - chriswarbo 8y ago
      Possibly this? http://www.macs.hw.ac.uk/~ek19/ML4PG/ http://www.macs.hw.ac.uk/~ek19/ML4PG/ It's mostly in maintenance mode (at least, I seem to have inherited its maintenance; and it's such a horrible mess of Emacs Lisp + Matlab + shell scripts that I don't dare touch it unless asked ;) ). It's used for clustering statements and proofs, the idea being that if you're stuck trying to prove something, you might be able to find something "similar" in an existing library to use as inspiration. It's mostly to help with manual searches, rather than automatically solving anything (although there is some related work on doing that for Coq called SEPIA https://arxiv.org/abs/1505.07987 https://arxiv.org/abs/1505.07987 and ACL2 http://www.macs.hw.ac.uk/~ek19/ACL2ml/index.html http://www.macs.hw.ac.uk/~ek19/ACL2ml/index.html ).
- forkerenok 8y ago
  The bottleneck is not the tool itself, but the theory it builds upon: Calculus of Constructs in Coq's case. CoC and other calculi oriented towards proofs have limitations. To better understand current challenges with provers I can recommend this episode of the Type Theory podcast with Dan Licata as a guest: http://typetheorypodcast.com/2015/01/episode-3-dan-licata-on-homotopy-type-theory/ http://typetheorypodcast.com/2015/01/episode-3-dan-licata-on... It's quite dense, but there are some bits that I, as a programmer, could understand.
  - Jweb_Guru 8y ago
    The vast majority of formal proofs don't run into any limitations with the CiC. They run into more practical limitations with the tooling and available libraries and tactics.
resters 8y ago
What is the painful part? The level of detail required for it to check?
- Retra 8y ago
  The painful part is that you're using tools which are trying to bridge between wildly different logical foundations. Just because a computer beeps and says "proof correct" doesn't mean you've proven what you thought you have, so we need to first translate the logic in which your assumptions are derived into the logic of the machine. That is a complex and subtle project. In other words, it's actually very easy to prove something with a computer, but it's very difficult to prove the thing you actually set out to prove. It's not any easier than writing a bug-free program.
  - singularity2001 8y ago
    Would it be possible to simplify the system by making default assumptions about a consensus/common-sense logic? Are topologists interested in different logical foundations?
    - alimw 8y ago
      You're right (and the GP isn't). A proof of your topological theorem in any one of Coq/Isabelle/Lean is a pretty good indication that it's correct, in spite of their various foundations.
      - Retra 8y ago
        ... assuming you correctly wrote your theorem in those frameworks.
        alimw 8y ago
        I think you are exaggerating the difficulty of theorem statement compared to proof. Here is one (admittedly extreme) example in Lean, from the formal abstracts website. theorem Wiles_Taylor : ∀ (x y z n : nat), x > 0 → y > 0 → n > 2 → x ^ n + y ^ n ≠ z ^ n := more years than I have to spare
ur-whale 8y ago
The fact that encoding Math proofs in a formal language is currently painful is well acknowledged. However, it shoudln't deter us from the goal. People used to code in assembly and Fortran. It was and still is quite painful. But programming languages have improved, and resorting to those original languages (which is what Coq is) is rarely necessary these days.

by bollu 8y ago

noisem4ker 8y ago

https://github.com/bollu/dependence-analysis-coq/blob/master/report-independent-study/independent-study.pdf https://github.com/bollu/dependence-analysis-coq/blob/master... Put a space before the final ), else it becomes part of the URL. Thanks for the paper, by the way.

WalterGR 8y ago

If you've ever tried encoding proofs in a proof assistant such as Coq... you'll realise just how painful it is Is that a result of how painful the tool is to use? (And by “tool” I mean any such tool - coq or whatever.) What would need to be improved in the state-of-the-art of automated proof validation for the process to be less painful?

patrickthebold 8y ago
Imagine convincing someone that a web service could be written, vs getting it written and deployed to production. And none of its dependencies actually exist either. Like someone just said... relational database? Yeah we could write one of those...
darkmighty 8y ago
> What would need to be improved in the state-of-the-art of automated proof validation for the process to be less painful? I think there are two parts: 1) Improve the theorem proving languages syntax so it's more intuitive, and so there is a wealth of "libraries" to build upon so you don't have to go from the basic axioms (of arithmetic or the reals for example) any time you wanted to prove something. 2) Provide some sort of computational intelligence to fill in natural gaps of proofs. I believe humans tend to leave a large number of more or less trivial gaps even in rigorous mathematical proofs that couldn't be avoided by language syntax. For this probably some kind of AI system would be ideal that tries to derive successive results and complete the proof automatically.
- AstralStorm 8y ago
  Isabelle semi-automatic theorem prover tries to help with 2 if you use sledgehammer strategy and print out the simplified proof with isar_proofs argument, which you can more easily read and reintegrate into the main document if needed. You can help its heuristics by providing it a set of potential proof facts explicitly. The libraries available for it are already quite huge... sometimes in a few encodings as well. (valued, typed, functional etc.) https://www.isa-afp.org/ https://www.isa-afp.org/
- anonlastname 8y ago
  I think coq has some kind of ml software. I saw it mentioned in the proof general UI. I'm not sure how good it is
  - chriswarbo 8y ago
    Possibly this? http://www.macs.hw.ac.uk/~ek19/ML4PG/ http://www.macs.hw.ac.uk/~ek19/ML4PG/ It's mostly in maintenance mode (at least, I seem to have inherited its maintenance; and it's such a horrible mess of Emacs Lisp + Matlab + shell scripts that I don't dare touch it unless asked ;) ). It's used for clustering statements and proofs, the idea being that if you're stuck trying to prove something, you might be able to find something "similar" in an existing library to use as inspiration. It's mostly to help with manual searches, rather than automatically solving anything (although there is some related work on doing that for Coq called SEPIA https://arxiv.org/abs/1505.07987 https://arxiv.org/abs/1505.07987 and ACL2 http://www.macs.hw.ac.uk/~ek19/ACL2ml/index.html http://www.macs.hw.ac.uk/~ek19/ACL2ml/index.html ).
forkerenok 8y ago
The bottleneck is not the tool itself, but the theory it builds upon: Calculus of Constructs in Coq's case. CoC and other calculi oriented towards proofs have limitations. To better understand current challenges with provers I can recommend this episode of the Type Theory podcast with Dan Licata as a guest: http://typetheorypodcast.com/2015/01/episode-3-dan-licata-on-homotopy-type-theory/ http://typetheorypodcast.com/2015/01/episode-3-dan-licata-on... It's quite dense, but there are some bits that I, as a programmer, could understand.
- Jweb_Guru 8y ago
  The vast majority of formal proofs don't run into any limitations with the CiC. They run into more practical limitations with the tooling and available libraries and tactics.

resters 8y ago

What is the painful part? The level of detail required for it to check?

Retra 8y ago
The painful part is that you're using tools which are trying to bridge between wildly different logical foundations. Just because a computer beeps and says "proof correct" doesn't mean you've proven what you thought you have, so we need to first translate the logic in which your assumptions are derived into the logic of the machine. That is a complex and subtle project. In other words, it's actually very easy to prove something with a computer, but it's very difficult to prove the thing you actually set out to prove. It's not any easier than writing a bug-free program.
- singularity2001 8y ago
  Would it be possible to simplify the system by making default assumptions about a consensus/common-sense logic? Are topologists interested in different logical foundations?
  - alimw 8y ago
    You're right (and the GP isn't). A proof of your topological theorem in any one of Coq/Isabelle/Lean is a pretty good indication that it's correct, in spite of their various foundations.
    - Retra 8y ago
      ... assuming you correctly wrote your theorem in those frameworks.
      - alimw 8y ago
        I think you are exaggerating the difficulty of theorem statement compared to proof. Here is one (admittedly extreme) example in Lean, from the formal abstracts website. theorem Wiles_Taylor : ∀ (x y z n : nat), x > 0 → y > 0 → n > 2 → x ^ n + y ^ n ≠ z ^ n := more years than I have to spare

ur-whale 8y ago

The fact that encoding Math proofs in a formal language is currently painful is well acknowledged. However, it shoudln't deter us from the goal. People used to code in assembly and Fortran. It was and still is quite painful. But programming languages have improved, and resorting to those original languages (which is what Coq is) is rarely necessary these days.