Huỳnh Trần Khanh (Dec 05 2022 at 16:29): Huỳnh Trần Khanh (Dec 05 2022 at 16:29):Hello. I've been learning formal verification for a while, and I'm reasonably proficient. But there's a catch though: I can't write informal proofs! There is a discrete math course in my university but the proofs are not as complicated as formal verification stuff. And I find it interesting that the standard advice in formal verification communities is think of how you prove stuff with pen and paper if you're stuck. I can unstuck myself by thinking more critically about the problem, but I can't write informal proofs because I'm not taught to do them. Is this normal?
Julien Puydt (Dec 05 2022 at 16:37):Yes: informal proofs try to convince humans ; formal proofs try to convince computers.
Théo Zimmermann (Dec 05 2022 at 16:44):This might become the new normal in times when students are taught less and less how to write proper pen and paper proofs. We're giving this piece of advice because in our own curricula, we've become used to writing pen and paper proofs well before we started doing formal verification. For someone with a different curriculum, things might be different. But the advice behind this really is to unplug the help that the computer is providing, to think critically and to try to get your own understanding of the problem guide your proof rather than just playing a game with a computer.
Meven Lennon-Bertrand (Dec 05 2022 at 17:30):The idea of this advice, as far as I can tell, is e.g. similar to the Rubber Duck technique common in software development, but has not much to do with knowing how to do pen-and-paper proof per se. It is mainly about taking a step back and trying to see the bigger picture
Paolo Giarrusso (Dec 05 2022 at 19:51):I wonder if this advice is comparable to "write pseudocode first"...
Paolo Giarrusso (Dec 05 2022 at 19:52):and possibly iterate back and forth between pseudo-proof and real proof
Paolo Giarrusso (Dec 05 2022 at 19:53):The conjecture is that in both cases, what's important is less "I'm using a standardized language" and more "I can sketch and iterate ideas without fill all the details a computer demands"
Paolo Giarrusso (Dec 05 2022 at 19:55):(there might be more to the advise for proofs; I can't quite tell)
Paolo Giarrusso (Dec 05 2022 at 19:55):otherwise, you risk for instance spending lots of time on a detailed proof for something that is (a) not true (b) true but not helpful (c) true and helpful, but on a convoluted proof strategy
Karl Palmskog (Dec 05 2022 at 20:10):well-run formalization projects have a high level informal "blueprint" for the statements/proofs they target, written before and during the formalization effort. Here is one example for the Lean Cap Set formalization.
Karl Palmskog (Dec 05 2022 at 20:15):other examples I can think of:
One could argue that machine-checked formalization gives rise to, and requires, informal proofs (and proof outlines) with different qualities than before.
Karl Palmskog (Dec 05 2022 at 20:19):also maybe relevant, recent paper with essay-style sections by people in ITP community and outside: https://arxiv.org/pdf/2207.04779.pdf ("Mathematical Proof Between Generations")
Yannick Forster (Dec 08 2022 at 09:20):@Huỳnh Trần Khanh you might want to try reading a more paper-based presentation of formal proofs. For instance MPCTT by Gert Smolka (https://github.com/uds-psl/MPCTT/) uses a diagram-based proof approach on paper, which will seem familiar to you if you have used Coq, but can be used as an intermediate step towards writing paper proofs
Yannick Forster (Dec 08 2022 at 09:27):Also, have a look at chapter 3.4.1 called "How to Translate a Proof Table" [to textual proofs] in the book "Introduction to Mathematics in Computer Science" (https://vorkurs.cs.uni-saarland.de/cms/ss22/dl/4/Book_Digital_Version.pdf) used to teach high-school students before starting to study at Saarland University. In general, I think the book provides a great introduction on how to learn writing textual proofs, both for students who do not know anything about proofs and for students who have a formal understanding of proofs. At least two of the authors are even here on Zulip: @Johannes Hostert @Christian Hagemeier
Karl Palmskog (Dec 08 2022 at 09:38):@Yannick Forster can you link to this intro book?
Yannick Forster (Dec 08 2022 at 09:38):Oops, yes, just forgot to: https://vorkurs.cs.uni-saarland.de/cms/ss22/dl/4/Book_Digital_Version.pdf
Karl Palmskog (Dec 08 2022 at 09:40):I think one general problem currently is that CS students only tend to see: (1) super-sloppy proofs in English ("one can easily see...") and (2) natural deduction proofs, maybe in Fitch style - and not much in between.
Karl Palmskog (Dec 08 2022 at 09:42):Lamport has some pretty nice ideas for getting some of the benefits of both in a hierarchical way (see his essay in the paper), but it doesn't seem to be all that popular
Michael Soegtrop (Dec 08 2022 at 10:50):There are some books where "the path is the goal". E.g. I have a German book called "Das Buch der Beweise" (the book of proofs) by Martin Aigner & Günter M. Ziegler, where the goal is not to proof X in the smallest number of words, but let's say to explore the beauty of mathematical proofs.
Notification Bot (Dec 08 2022 at 20:27):10 messages were moved from this topic to #Miscellaneous > Do mathematicians really care about truth? by Paolo Giarrusso.
Last updated: May 31 2023 at 04:01 UTC