32 ms·

Formal Proof Sketches (2003) [pdf]

30 points by larve 4y ago

fspeech 4y ago
We need to develope tools that can automatically fill small gaps (ones left as errors in the essay), because the point of having mechanized proofs is to not have gaps. Then practitioners can write lemmas and let the computers do the checking.
- reuben364 4y ago
  In the proof assistants I'm familiar with, such as Lean and Coq, you can write tactics which generate proofs for a goal and potentially produce more subgoals. However there isn't a "one size fits all" tactic for these gaps. One area that is being explored is ML for generating proofs, but training data is limited.
  - fspeech 4y ago
    The tactics still require users to be aware of their existence and using them correctly (a non trivial mental load). And the resulting proof script is brittle and hard to read. This is what the essay attempted to improve over.
    - mbrodersen 4y ago
      Automated tools like Sledgehammer (Isabell/HOL) removes a lot of the manual work.
      - fspeech 4y ago
        I have not used Sledgehammer but even with a SAT solver we still need to handle quantifier instantiations. And in case the SAT solver fails (I mean time-outs, not finding counter-examples) we won't get clues on how to fix it. SAT solvers work on CNF, which is very far from the deeply structured formulaes that math tends to generate.
        mbrodersen 4y ago
        I am not a working mathematician and don’t care about formalising mathematics. For the things I do care about (proving code correct) tools like Sledgehammer are awesome.
- mbrodersen 4y ago
  Dafny is a great example of what you are talking about. It automated most of the proving. However you still need to figure out the key invariants.
pflanze 4y ago
(I'm a software developer, not a mathematician. I'm just starting to try to understand the proof world.) I'm not sure about the "disdain" the authors have about "program source code". The parallel between proofs and programs seems clear, a runnable program is only one for which all functions/subroutines/methods (in other words, abstractions) have been implemented. We try to structure programs so that the abstractions are as sensible as possible, with good, preferably memorable names. A well-written program is one where the higher level is short and understandable without (always) having to dive into what the used abstractions do. It is an aim we seem to share with the writers of the paper. Sure, real world might be different, but the technology allows us to write well-readable programs. Other attempts like UML/flowcharts exist, but AFAIK attempting to connect these to runnable programs (i.e. make them formal program sketches in the sense of the proof sketches in the linked paper) has largely been a failure (correct me if I'm wrong). The idea to write the program and mark the parts that should show up in a flowchart (i.e. the inverse of what I've mostly seen talked about, program generation from UML), to get a "human readable" version of the program, might be a new one. Maybe if mathematicians succeed with that, it would be as applicable to software engineering? In any case, am I correct in saying that the envisioned aim is the same? Does mathematics have peculiarities that make the situation different (other than, perhaps, mathematicians generally not being used to "programming", or fully formalizing something)? Is this a "teething" stage in mathematics like UML was in software engineering and will largely be superseded by just "structuring programs/proofs well", which entails creating "nice libraries"? PS. I have ignored that the paper is from 2003 (about the time of UML's heyday, incidentally). What has happend to the idea of proof sketches in the mean time? Is this what "tactics" is about?
- fspeech 4y ago
  You may be interested in the Curry-Howard correspondence https://en.m.wikipedia.org/wiki/Curry–Howard_correspondence https://en.m.wikipedia.org/wiki/Curry–Howard_correspondence Tactics can be thought of functions that manipulate proof contexts (e.g. sequent calculi https://encyclopediaofmath.org/wiki/Gentzen_formal_system https://encyclopediaofmath.org/wiki/Gentzen_formal_system). Tactical proof is like imperative programming where one specifies explicitly how a proof should be constructed. Ideally we want to move towards declarative proofs, where one specifies lemmas that can be checked automatically. To be exact, suppose H1, ..., Hn are hypotheses (including known axioms and theorems), we want to derive Th by finding a sequence of propositions L1 ... Lm (=Th) such that L_(i+1) can be derived automatically from the hypotheses plus L1 through Li.
mbrodersen 4y ago
> formalizing mathematics currently seems far too much work to be worth the time of the working mathematician A very general statement that isn’t true in all cases. I recommend taking a look at the LEAN mathlib project. It is a group of working mathematicians proving leading edge mathematics correct using a formal proof tool (LEAN). The problem with leading edge mathematics seems to be that the proofs are too complex for anybody but a few specialists to verify the traditional way. And those specialists are already busy working on their own proofs. So having an automated assistant verifying the proofs seems to be necessary for the future of mathematics. I am not a working mathematician myself however that is the impression I am getting reading articles written by leading edge working mathematicians. The same way that large complex software applications are too complex for humans to verify without the help of automated proof tools.
- fspeech 4y ago
  When Hales started in 2003 the Flyspeck project https://github.com/flyspeck/flyspeck https://github.com/flyspeck/flyspeck to formally verify his own proof of the Kepler conjecture he likely didn't know that it would take him (and a team of helpers later) until 2014 to finish. He used hol-light, which is very much geared towards proof automation. Lean is more expressive (being dependently typed) but I am not aware of any real advance in automation over hol-light. Indeed with their focus on code generation (therefore constructive logic) and software verification, proof automation for math is likely harder in Lean. But the expressiveness and good tooling seem to have generated a lot of interests and mathlib has a real active community, which is really good to see.
  - mbrodersen 4y ago
    Yep agree. Having an active team of working mathematicians and field medalists giving feedback to the LEAN development team is really helpful in pushing automation forward. Having said that, for people like me, who doesn’t care about formalising mathematics but do care about proving code correct, proof automation has already come a long way and is on the edge of becoming a practical tool for highly critical software.

30 points by larve 4y ago

We need to develope tools that can automatically fill small gaps (ones left as errors in the essay), because the point of having mechanized proofs is to not have gaps. Then practitioners can write lemmas and let the computers do the checking.

reuben364 4y ago
In the proof assistants I'm familiar with, such as Lean and Coq, you can write tactics which generate proofs for a goal and potentially produce more subgoals. However there isn't a "one size fits all" tactic for these gaps. One area that is being explored is ML for generating proofs, but training data is limited.
- fspeech 4y ago
  The tactics still require users to be aware of their existence and using them correctly (a non trivial mental load). And the resulting proof script is brittle and hard to read. This is what the essay attempted to improve over.
  - mbrodersen 4y ago
    Automated tools like Sledgehammer (Isabell/HOL) removes a lot of the manual work.
    - fspeech 4y ago
      I have not used Sledgehammer but even with a SAT solver we still need to handle quantifier instantiations. And in case the SAT solver fails (I mean time-outs, not finding counter-examples) we won't get clues on how to fix it. SAT solvers work on CNF, which is very far from the deeply structured formulaes that math tends to generate.
      - mbrodersen 4y ago
        I am not a working mathematician and don’t care about formalising mathematics. For the things I do care about (proving code correct) tools like Sledgehammer are awesome.
mbrodersen 4y ago
Dafny is a great example of what you are talking about. It automated most of the proving. However you still need to figure out the key invariants.

pflanze 4y ago

(I'm a software developer, not a mathematician. I'm just starting to try to understand the proof world.) I'm not sure about the "disdain" the authors have about "program source code". The parallel between proofs and programs seems clear, a runnable program is only one for which all functions/subroutines/methods (in other words, abstractions) have been implemented. We try to structure programs so that the abstractions are as sensible as possible, with good, preferably memorable names. A well-written program is one where the higher level is short and understandable without (always) having to dive into what the used abstractions do. It is an aim we seem to share with the writers of the paper. Sure, real world might be different, but the technology allows us to write well-readable programs. Other attempts like UML/flowcharts exist, but AFAIK attempting to connect these to runnable programs (i.e. make them formal program sketches in the sense of the proof sketches in the linked paper) has largely been a failure (correct me if I'm wrong). The idea to write the program and mark the parts that should show up in a flowchart (i.e. the inverse of what I've mostly seen talked about, program generation from UML), to get a "human readable" version of the program, might be a new one. Maybe if mathematicians succeed with that, it would be as applicable to software engineering? In any case, am I correct in saying that the envisioned aim is the same? Does mathematics have peculiarities that make the situation different (other than, perhaps, mathematicians generally not being used to "programming", or fully formalizing something)? Is this a "teething" stage in mathematics like UML was in software engineering and will largely be superseded by just "structuring programs/proofs well", which entails creating "nice libraries"? PS. I have ignored that the paper is from 2003 (about the time of UML's heyday, incidentally). What has happend to the idea of proof sketches in the mean time? Is this what "tactics" is about?

fspeech 4y ago
You may be interested in the Curry-Howard correspondence https://en.m.wikipedia.org/wiki/Curry–Howard_correspondence https://en.m.wikipedia.org/wiki/Curry–Howard_correspondence Tactics can be thought of functions that manipulate proof contexts (e.g. sequent calculi https://encyclopediaofmath.org/wiki/Gentzen_formal_system https://encyclopediaofmath.org/wiki/Gentzen_formal_system). Tactical proof is like imperative programming where one specifies explicitly how a proof should be constructed. Ideally we want to move towards declarative proofs, where one specifies lemmas that can be checked automatically. To be exact, suppose H1, ..., Hn are hypotheses (including known axioms and theorems), we want to derive Th by finding a sequence of propositions L1 ... Lm (=Th) such that L_(i+1) can be derived automatically from the hypotheses plus L1 through Li.

mbrodersen 4y ago

> formalizing mathematics currently seems far too much work to be worth the time of the working mathematician A very general statement that isn’t true in all cases. I recommend taking a look at the LEAN mathlib project. It is a group of working mathematicians proving leading edge mathematics correct using a formal proof tool (LEAN). The problem with leading edge mathematics seems to be that the proofs are too complex for anybody but a few specialists to verify the traditional way. And those specialists are already busy working on their own proofs. So having an automated assistant verifying the proofs seems to be necessary for the future of mathematics. I am not a working mathematician myself however that is the impression I am getting reading articles written by leading edge working mathematicians. The same way that large complex software applications are too complex for humans to verify without the help of automated proof tools.

fspeech 4y ago
When Hales started in 2003 the Flyspeck project https://github.com/flyspeck/flyspeck https://github.com/flyspeck/flyspeck to formally verify his own proof of the Kepler conjecture he likely didn't know that it would take him (and a team of helpers later) until 2014 to finish. He used hol-light, which is very much geared towards proof automation. Lean is more expressive (being dependently typed) but I am not aware of any real advance in automation over hol-light. Indeed with their focus on code generation (therefore constructive logic) and software verification, proof automation for math is likely harder in Lean. But the expressiveness and good tooling seem to have generated a lot of interests and mathlib has a real active community, which is really good to see.
- mbrodersen 4y ago
  Yep agree. Having an active team of working mathematicians and field medalists giving feedback to the LEAN development team is really helpful in pushing automation forward. Having said that, for people like me, who doesn’t care about formalising mathematics but do care about proving code correct, proof automation has already come a long way and is on the edge of becoming a practical tool for highly critical software.