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?
Yes: informal proofs try to convince humans ; formal proofs try to convince computers.
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.
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
I wonder if this advice is comparable to "write pseudocode first"...
and possibly iterate back and forth between pseudo-proof and real proof
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"
(there might be more to the advise for proofs; I can't quite tell)
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
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.
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.
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")
@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
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
@Yannick Forster can you link to this intro book?
Oops, yes, just forgot to: https://vorkurs.cs.uni-saarland.de/cms/ss22/dl/4/Book_Digital_Version.pdf
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.
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
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.
Quote from book Yannick linked:
To do mathematics, we need to figure out whether our statements are true.
This sounds like constructivism to me. Isn't the usual classical view something like: "we need to ensure that our statements are not inconsistent"
I‘m not sure whether a classical mathematician would see a difference between „true“ and „not inconsistent“ statements.
10 messages were moved from this topic to #Miscellaneous > Do mathematicians really care about truth? by Paolo Giarrusso.
Last updated: Jan 29 2023 at 19:02 UTC