[HN Gopher] Basics of Proofs (2017) [pdf]
___________________________________________________________________
Basics of Proofs (2017) [pdf]
Author : waldarbeiter
Score : 127 points
Date : 2023-06-16 08:34 UTC (1 days ago)
(HTM) web link (theory.stanford.edu)
(TXT) w3m dump (theory.stanford.edu)
| herodotus wrote:
| I did my undergraduate degree at Wits University in Johannesburg.
| My Real Analysis course was SO boring. The lecturer basically
| wrote on the board:
|
| Lemma: ......
|
| Proof: ....
|
| etc.
|
| Theorem: Let epsilon < K, ....
|
| Proof: ....
|
| --QED--
|
| which we all dutifully copied into our notebooks. Very
| uninspiring.
|
| But when I got to the University of Waterloo for graduate
| studies, I had a real competitive advantage over my peers for the
| theory courses I took: I knew what a proof was, and how to do
| one.
| WoahNoun wrote:
| I think the problem a lot of people have (even math majors) is
| expecting the lecture to be the first introduction to the
| topic. It's like taking a literature class and going to lecture
| without doing the reading. Reading (or even just skimming) the
| next section/chapter of the book before the lecture allows you
| to focus and ask questions on the parts of the material you
| didn't understand during the lecture. I very rarely wrote down
| full proofs in my notes during the lecture. I focused on the
| lecture itself and wrote down the pieces that I wanted to
| remember.
| constantcrying wrote:
| >which we all dutifully copied into our notebooks. Very
| uninspiring.
|
| I had 5 years of that, a very enjoyable time.
| Solvency wrote:
| It's intriguing to me that someone who made it to Stanford might
| only just be getting exposed to the basics of proofs like this?
| mbg721 wrote:
| It makes some sense to have a leveling-of-expectations course
| for freshmen that both inflates their GPA and says "Okay,
| whatever you were told in high school, we expect you to use
| this."
| sukilot wrote:
| [dead]
| cubefox wrote:
| Affirmative action and many related criteria mean that students
| aren't just admitted by considerations of ability.
| a1o wrote:
| For some reason I thought it would be about Coq or other similar
| structured proof assistant language.
| btilly wrote:
| I still prefer the explanation that I prepared when I was
| teaching at Dartmouth College.
|
| https://docs.google.com/document/d/1_uwl3WDZk_BxNOUL7W0FiPMM...
|
| I literally gave everyone that handout and told them, "To make
| sense of it, you're all going to do the next proof. I'll just
| prompt you." They thought this was impossible. But I told them to
| trust me and I began.
|
| I went around the room. I asked one person what the next step in
| the flowchart was. I asked the next person to do it. I just wrote
| down what they said. Kept going until they had produced a
| complete proof of a result that, at the beginning, they did not
| know why it might be true.
|
| The best comment I got from that class later was, "Proofs are
| easy. It is kind of like filling out a shopping list."
| mjw1007 wrote:
| Maybe it's worth one more section near "Any Ideas On Why It Is
| True?", something like:
|
| Are you beginning to doubt whether it's true?
|
| Try to think of a counterexample.
|
| Is there something that keeps getting in the way of a
| counterexample working? Can you prove that that always happens?
| btilly wrote:
| Read the second paragraph of the description of "Any Ideas On
| Why It Is True?"
|
| :-)
| nohaydeprobleme wrote:
| This is fantastic. Perhaps similarly, I personally found it
| much easier to complete math problem sets after I began to
| write out an explicit list of steps of what to do.
|
| For example, I broke down problems with to-dos, such as:
|
| 1. Find the definition for what math_term_X means in a
| particular problem.
|
| 2. (For breaking down part of the problem): Figure out how to
| show that a particular object is lesser than or equal to
| another project.
|
| 3. Write down headings for each case I need to prove.
|
| ...and so on.
|
| Writing down explicit steps was far more practically helpful to
| me, than my previous conception of problem-solving from the
| quote about how Feynman solves problems (that is: "Write down
| the problem, think real hard, write down the solution"). Some
| people may not need to write down steps, but I was personally
| able to learn a lot more with a specific, more verbalized
| approach.
|
| It's very neat and helpful to have a flowchart suited to any
| general problem, which I'll try out in addition to my current
| approach of writing down a list of to-dos for solving specific
| problems. Thanks a lot for sharing.
| getpost wrote:
| Nice and concise! I just started Proof and the Art of Mathematics
| by JD Hamkins[0], based on pg's recommendation[1], "is a
| beautiful book in both senses. It's both beautifully written, but
| also physically beautiful, thanks to its many illustrations,
| which I was surprised to hear were made by the author himself."
| Chapter 4 on induction improved my attitude.
|
| [0]https://www.amazon.com/Proof-Art-Mathematics-Examples-
| Extens... [1]
| https://twitter.com/paulg/status/1662065331727155202
| tromp wrote:
| I found Johannes Riebel's thesis [1] an excellent introduction to
| the formalization of Zermelo Fraenkel-Set theory, complete with
| detailed examples of formal proofs.
|
| [1] https://www.ingo-blechschmidt.eu/assets/bachelor-thesis-
| unde...
| tigerlily wrote:
| There's also "proof by picture", in which you can hastily attempt
| to prove or disprove something by drawing a suitable diagram in
| your exam booklet. You have to be darn sure of what you're doing
| though... ;)
| constantcrying wrote:
| Ironically when rigorous proofs were invented by the greeks,
| Euclids "proof by picture" was no less rigorous than modern
| formal logic.
| YeGoblynQueenne wrote:
| Right now this article is at no. 10 on the front page, while no.
| 11 is "Book of Proof (2018)".
|
| This is the third time I notice such a coincidence on HN. Is this
| something that HN does on purpose? Like, does the site match
| posts with similar titles on the front page to encourage
| discussion in both? Note that (at the time of writing) this
| article has 91 points and the other one 45, so the two articles
| are not ordered by upvote count.
|
| Also, I need a catchy name for this phenomenon (just 'cause I
| want to name the folder where I keep screenshots documenting it,
| like). Suggestions?
| constantcrying wrote:
| >Is this something that HN does on purpose?
|
| No, the HN algorithm is extremely simple and does not consider
| syntactic similarities of the titles.
| Solvency wrote:
| I've noticed similar themed posts appearing in clusters
| constantly on HN. It's way too commonplace to be
| coincidental.
| constantcrying wrote:
| No it is coincidental. Look at the algorithm yourself.
| Solvency wrote:
| It doesn't mean it's the algorithm, it means users could
| be tactically posting to ride a wave of similar interest.
| That's all.
| constantcrying wrote:
| Yes, you are right. Potentially the effect is partly due
| to that after seeing the first post a user stumbles over
| something related and decides to post that as well.
| waldarbeiter wrote:
| I was not aware of the other post when posting this. I stumbled
| upon this PDF coincidentally and thought it would be valuable
| for HN.
| Jtsummers wrote:
| The _Book of Proof_ post was made 2 hours after this one, you
| wouldn 't have been aware of it. It happens a lot. See a
| topic, and people post related things because it jogs a
| memory, they found it while digging deeper, or as a form of
| indirect response.
| Jun8 wrote:
| Over the years I've noticed it too, the time lag between
| similar posts ranging from a few hours to a day or so. My
| simple explanation is that a person reading the original post
| either remembers a related nugget of Internet that they think
| people would also find interesting or else they find it while
| googling, inspired by the initial post.
| cubefox wrote:
| When I was first introduced to mathematical proofs, I was
| perplexed by how fuzzy and intuition-based the notion of proof
| was. A "convincing argument", really?! There is no knowing, as a
| novice, how detailed those "arguments" have to be, what parts you
| can simply assert without further justification. Usually the
| teachers themselves can't explain what the criteria for an
| "obvious" and "not obvious" step is, they just know it
| intuitively from experience. Writing proofs, then, is a lot like
| having to learn to ride a bike: Instructions are mostly
| unavailable or useless.
|
| I later learned that there is indeed a precise way of learning
| proofs which doesn't rely on intuitions of what counts as a
| rigours inference step: Formal logic together with a natural
| deduction proof system. Natural deduction is a formal proof
| system which resembles actual ("natural") proofs in mathematics,
| unlike other proof systems.
|
| In such a proof system, inference rules, like modus tollens or
| universal instantiation, are strictly defined. Only the given
| inference rules (and those which are provable from the given
| rules) may be used. Coming up with such proofs still requires
| creativity, there is no algorithm. But there is no ambiguity in
| what counts as a valid or invalid proof or inference step.
|
| Of course, this is far too tedious for actual mathematical
| proofs, since every little step needs to be done explicitly, e.g.
| even applications of modus ponens (rule: "A, if A then B,
| therefore B"). Moreover, mathematicians rarely prove anything
| from axioms, they start from other statements which are
| considered more trivial. But I think it would be helpful for many
| people to first learn logic and deduction "the precise way", and
| _then_ do actual mathematical proof where you can jump over more
| obvious parts.
|
| But that's not how it is teached in mathematics or computer
| science. Students are thrown into the cold water, and only
| receive tips&tricks, but no rigorous introduction. Ironically,
| the one subject which often teaches formal logic as an early
| introductory class for undergraduates isn't mathematics, computer
| science, or physics, it's philosophy.
| checkyoursudo wrote:
| Philosophy was the only field where I learned formal logic at
| all. I went into higher math, did some CS, and also got a law
| degree[1], and am now doing a Ph.D. in informatics, and still
| the only place I have _really_ been exposed to formal logic was
| my undergrad degree in philosophy.
|
| [1] It is amazing (or not, depending on your view of lawyers)
| that lawyers are basically not taught anything about making and
| proving formal arguments, at least in my experience.
| lixtra wrote:
| Law is not about logic. It's about hermeneutics. It's closer
| to religion than to math.
| Solvency wrote:
| Which is why the most successful lawyers are more akin to
| the most successful evangelists: the ability to hoodwink
| groups of people with their interpretation.
| constantcrying wrote:
| > But I think it would be helpful for many people to first
| learn logic and deduction "the precise way", and then do actual
| mathematical proof where you can jump over more obvious parts.
|
| Absolutely. And I can not imagine a mathematics degree which
| doesn't place formal logic front and center in the first
| semester. When you are starting out you absolutely need to
| suffer through the rigourous formal arguments.
|
| >Ironically, the one subject which often teaches formal logic
| as an early introductory class for undergraduates isn't
| mathematics, computer science, or physics, it's philosophy.
|
| I can not believe that this is the case. Even engineering
| undergrads have to learn formal logic in their first semester.
| sukilot wrote:
| Formal logic is taught in Mathematical Logic class
| (intermediate, optional) or Discrete math
| (intro/intermediate, often not taken)
|
| Geometry class in high school sometimes teaches some of it.
|
| Computer science Binary logic teaches some of (De Morgan's
| laws)
|
| Outside of New Math of the 1970s, it is a glaring omission
| from the curriculum.
|
| Even enriched classes like Art of Problem Solving that put
| heavy emphasis on proofs, do not teach formal logic.
| 141205 wrote:
| > Even engineering undergrads have to learn formal logic in
| their first semester.
|
| I got my engineering B.S. from a top 5 college in the US, and
| have known many people who have gone to similar schools. None
| of us have had to take a class that goes into first order
| logic or proof writing. I don't know what college you go to
| where that is a thing, but it would be exceedingly rare.
| daniel-cussen wrote:
| [dead]
| constantcrying wrote:
| >I don't know what college you go to where that is a thing,
| but it would be exceedingly rare.
|
| German technical university. I was a tutor there. AFAIK
| this is normal.
|
| As part of the first semester you take linear algebra and
| analysis, starting out with the basics of formal logic. Of
| course the courses are less focused on proof writing than
| the mathematics "major" courses.
|
| I should also point out that German universities have very
| loose entry standards (except when places are very rare
| compared to applicants) and use the first two semesters to
| filter out students. These courses are often designed to
| have around a 50% failure rate.
| Solvency wrote:
| Your student filtration system sounds like a long and
| expensive waste of everyone's time.
| constantcrying wrote:
| Not really. First year courses usually have hundreds of
| students in large halls. There is some more effort as you
| need more tutors, but that is basically it. (Students
| usually do not live on campus)
|
| The enormous upside is that all students are judged
| equally on their ability to academically succeed in their
| chosen field. I think US university admissions are
| ridicolous for many reasons.
| l33t233372 wrote:
| > As part of the first semester you take linear algebra
| and analysis, starting out with the basics of formal
| logic
|
| There is not enough time to learn the basics of formal
| logic and linear algebra and/or analysis in a single
| class, but I think what you're referring to is an
| introduction to proof techniques like induction, modus
| tollens, quantifiers, etc.
|
| Every math and computer science department in the US that
| I've ever heard of teaches these topics, but I wouldn't
| call it a formal logic class.
| constantcrying wrote:
| For me basic formal logics means learning the symbols
| (conjunction, disjunction, implication, equivalency, not,
| etc.) and the rules of inference to maniuplate these
| symbols and using these rules to prove new things.
|
| How can you teach analysis without that anyway. It is
| absolutely essential for set theory and how would you
| e.g. define the reals (in a "proper" math course, not
| engineering) without a good understanding of set theory?
|
| If you don't believe me, here is a link to the contents
| of a first semester engineering math course from some
| german technical university: https://page.math.tu-
| berlin.de/~joswig/teaching/notes/Joswig...
|
| The symbols should be enough to tell you what the
| contents are.
| auggierose wrote:
| I like your analogy with riding a bike: If you want to ride a
| bike, what is more important, learning how to ACTUALLY DO IT,
| or to learn the physical and mechanical rules underlying it?
| Furthermore, technical knowledge will always be incomplete (and
| that applies also to logic in a very technical sense), while
| once you learnt how to ride a bike, your knowledge, in a way,
| is complete.
| cubefox wrote:
| A lot of things _can_ be learned simply by practice, without
| any theory, but many things at least benefit from learning it
| in a more principled way. That 's not feasible for riding
| bikes, since this relies on the the motor cortex, which
| doesn't understand and benefit from explicit knowledge about
| the physics of bike movement. Writing proofs is more
| intellectual, it benefits from principled understanding.
| auggierose wrote:
| Finding theorems and proofs is not intellectual at all, it
| is like riding a bike. You are probably not going to prove
| anything new and interesting by approaching it from an
| intellectual angle. You CAN turn it into an intellectual
| exercise, and at some point it is very beneficial to do so,
| for meta-mathematical insights. Just like it is beneficial
| to learn the physics and mechanics of cycling, if you want
| to construct bikes. It's also very helpful when you are
| wondering about the technical veracity of your theorems and
| proofs. It's not that helpful if you want to FIND those
| theorems and proofs in the first place. Starting out with a
| fixed rule system also has the danger of limiting your
| imagination about what's possible, given that no fixed rule
| system is ever going to be enough.
| cubefox wrote:
| Proving things with formal calculi still relies on
| something like creativity, which itself isn't captured by
| a precise algorithm, similar to informal proofs. The
| advantage of learning formal proof is, I claim, purely
| didactic, as it gives a clear idea on what a valid
| inference step is _in the ideal case._ I don 't think
| there is really a danger of limiting your imagination, as
| you will probably stop thinking in formal terms as soon
| as you are good in doing informal proofs.
|
| For example, the above Stanford document on proof basics
| doesn't even mention elementary inference rules like
| modus tollens. It briefly refers to "the contrapositive",
| but without explaining what the contraposition rule even
| is. It was clearly written by someone who regards all
| these as too obvious to be mentioned in such a document
| (he only explains proof by contradiction), but they are
| not obvious to novices.
|
| Anyway, your comment reminds of an interesting paper[1]
| by Yehuda Rav, where he defends the autonomy of informal
| proof with original arguments against the "formalists".
| You might be interested, I think your intuitions are
| going in a similar direction.
|
| [1]
| http://sgpwe.izt.uam.mx/files/users/uami/ahg/1999_Rav.pdf
| auggierose wrote:
| Thanks for the link, looks like an interesting paper!
|
| The thing is, formal rules can only model what you
| already understand. A formal rule can tell you exactly
| WHAT and HOW, but not WHY. But especially with basic
| proof rules like modus ponens, that is essential. So
| intuitive understanding is prior to formal rules. Of
| course, lots can be gained from the interplay of
| intuition and formality, I am the last one to deny that.
|
| For me, that is an important issue, because I am a big
| proponent of doing logic on the computer, which
| necessarily is formal. Nevertheless, the goal here is to
| make logic on the computer as intuitiv as possible,
| something many people in the field don't seem to have a
| desire for. I also don't want the next generation to
| think exclusively in formal systems, in terms of, oh, if
| my formal system doesn't allow that, what I want to do
| must be wrong, or at least stupid. There is already
| enough of that going around with type theorists.
| hiatus wrote:
| > When I was first introduced to mathematical proofs, I was
| perplexed by how fuzzy and intuition-based the notion of proof
| was.
|
| This was precisely my issue when studying proofs in school. Do
| you have any suggestions for resources to get started down the
| right path?
| cubefox wrote:
| The lecture notes for some introductory logic class of an
| analytic philosophy department may be quite good, but
| unfortunately I can't recommend something specific for
| English.
| yep31 wrote:
| >some introductory logic class
|
| like forall x from openlogicproject?
| vkazanov wrote:
| "How to prove it" is the best book you can find
| hackermailman wrote:
| Some universities now have a Lean proof assistant logic course
| that teaches natural deduction
| http://leanprover.github.io/logic_and_proof/
|
| Whenever I have asked professors in the past how they first
| learned proofs the answer was always from doing Euclid in
| highschool which is no longer taught
| cubefox wrote:
| That course looks like a great introduction!
|
| (A small downside is, in my opinion, that is uses trees
| instead of a more classical sequential presentation in the
| style of Suppes and Kleene.
|
| https://en.wikipedia.org/wiki/Natural_deduction#Different_pr.
| ..
|
| Trees may be more elegant, but actual, informal proofs in
| mathematics are written sequentially. So I think trees defeat
| the purpose of "natural" deduction a bit. But that's
| complaining on a high level.)
| vkazanov wrote:
| I studied CS and electric engineering for 6-7 years total, and
| both degrees included some pretty math-intense courses, proofs
| and all. I remember how I really, really wanted an explanation
| of the underlying proof system but all I got was just more
| intuitive explanations, all of which felt out of place.
|
| What is unusual is that I kept looking. "How to Prove It" was
| something I really wish I read ahead of calculus. It is only
| after this book it clicked for me, all of it. Having understood
| the rules of the game it became possible to play with math..!
| Which I still do from time to time.
|
| I think that this material should be taught at high school.
| Bits of it even earlier.
| ithinkso wrote:
| > Moreover, mathematicians rarely prove anything from axioms,
| they start from other statements which are considered more
| trivial.
|
| Not more trivial but from the ones already proved and those
| closer to the thing you are proving. There is no need to go
| back to the axioms if you know, and can reference, proof of
| step N-1, just go from there.
|
| There is also this 'misconception' that mathematical theorems
| follow from the axioms. They do, of course, but the axioms were
| choosen just right to make things that were working to still
| work, with some weird consequences like axiom of choice
| cubefox wrote:
| There are are a lot of "folk theorems" in mathematics, and
| things which are simply considered obvious or common
| knowledge relative to a conjecture in question, without
| anyone being able to actually cite a proof for that.
| Mathematical proof is really just for convincing other
| mathematicians, there is no need to prove things which are
| considered obvious.
| constantcrying wrote:
| >There are are a lot of "folk theorems" in mathematics
|
| Can you name some? Preferably in analysis.
| rdlw wrote:
| I found this, unfortunately it is about category theory:
| "manuscripts [...] that are cited but never became widely
| available"
|
| https://ncatlab.org/nlab/show/list+of+lost+manuscripts+in
| +ca...
| constantcrying wrote:
| Any particular _theorem_? This links to hard /impossible
| to access materials, but does any of them actually
| contain a theorem which proof is not accessible in some
| form?
|
| Further is it any _relevant_ theorem, which has been
| cited many times?
| rdlw wrote:
| From the link I posted:
|
| John Beck's Monadicity Theorem is cited in "many sources"
| but a manuscript has been found and "The proof is
| reproduced for instance in (MacLane, p. 147-150, Riehl
| 2017, 5/5/)".
|
| Fred Linton cites Michael Barr for a "Universal property
| of the Kleisli construction" and no copy has been found.
|
| I don't know enough about the subject to say how
| difficult these proofs would be to recreate or whether
| they exist elsewhere, but these definitely seem to be
| specific theorems.
|
| I'd like to see a specific theorem in any field that was
| once proven and accepted but all existing proofs have
| been lost. That would be extremely tantalizing
| constantcrying wrote:
| I don't think this is convicing at all. None of this
| shows that there are generally accepted theorems without
| proofs.
|
| The first one isn't lost at all, the second is just a
| single lost citation.
|
| All of this is very far away from mathematicians building
| upon thr shaky grounds of mythical theorems. Also, in all
| my mathematical experience (going up to recent research
| in analysis) I never encountered something like this. In
| all textbooks I ever read either everything was proven or
| was cited to other works, which every time I checked
| included the proof.
| ithinkso wrote:
| None of what you said is true except for
|
| > Mathematical proof is really just for convincing other
| mathematicians
|
| which is _precisely_ the point of a proof, but 'convince'
| means something different than you seem to think it means
| (in the field of mathematics)
| spacemadness wrote:
| Our discrete mathematics professor leaned heavy on proofs, but
| also introduced pop quizzes for proofs of algorithms and other
| mathematical constructs as an experiment that term which sent
| my anxiety ablaze. You either had the intuition for that
| particular problem or you didn't. Studying would not help you
| that much. The success rate on the quizzes was very low
| surprising no one.
| StrangeATractor wrote:
| Classes like this were funny. I often found that people who
| just knew the answer immediately had a lot of difficulty
| doing proofs, and the people good at doing proofs usually
| didn't arrive at the solution very quickly or seem to have an
| intuitive understanding of the problem at first.
|
| Some people are just wired differently.
| dvwobuq wrote:
| That's interesting. In your context what is "knowing the
| answer"? To me it seems like they "knew" a given statement
| was true but they didn't know how to prove it which makes
| me wonder how they knew.
| StrangeATractor wrote:
| The teacher may start off a class with a question like
| "what is the most efficient way to satisfy this problem
| given these constraints?" Some people would know the
| answer immediately but couldn't do a proof for it hardly
| at all. Others could find a proof in class almost every
| time, but necer really saw the answer to the problem
| until they'd sat on it for a while and chewed over it.
|
| Can't really give an example question, it's been well
| over a decade (closer to two) since I took it.
___________________________________________________________________
(page generated 2023-06-17 23:01 UTC)