Proofs from the book

Stream: general

[Moritz Firsching]

I thought it would be fun to formalize some parts of the book "Proofs from the book" by Aigner/Ziegler and started this github-repo for this:
https://github.com/mo271/formal_book
In general the statements and proofs are quite accessible and span a wide variety of topics, so I expect some parts to be quite easy to do with what is already present in mathlib, while other parts might be significantly harder. Also some of the chapters might be nice projects for undergraduates.
Contributions/suggestions for improvements are most welcome!

[Kevin Buzzard]

Are some proofs in that book pictures? I was looking through a book called "proofs without words" and some of those proofs are very elegant but they would be really really hard to formalise!

I now have a limited experience with getting undergraduates to formalise a book, because I made this repo https://github.com/ImperialCollegeLondon/m1fexplained over the summer, which is a formalisation of some (and hopefully one day most) of the exercises in a standard undergraduate textbook written by my boss! (Martin Liebeck, the head of pure maths at Imperial, and someone who I owe a lot to because five years ago I started doing this weird new thing called Lean and he was totally fine about it). One thing I learnt is that if you want to get undergraduates involved, they're far more likely to embark on something if there's a sorried statement. So if you want to make the project grow organically and are happy to put some effort into an initial push I would thoroughly recommend sorrying a whole bunch of theorem statements. It's easy to forget how hard this part of the job is, once you're good at it. Most of the code in that repo was written by Imperial undergrads over the summer.

[Yaël Dillies]

docs#symm_diff_assoc is a proof from Proofs of the book.

[Kevin Buzzard]

What has happened with mathlib is that at the beginning undergraduates were really useful to us. There was a ton of stuff which needed to be done, and in some sense undergraduates were even sometimes directing what got done, there were people like Chris Hughes and Kenny Lau who were immersed in Imperial's undergraduate degree and were formalising parts of it and responding to other undergraduates who wanted to do things like problem sheet questions. Now mathlib is beyond this point. The stuff on the UG todo list typically cannot be done by beginner UGs any more, for the simple reason that there's nothing easy left; everything is difficult/annoying for one or more reasons and the problems are beyond a beginner. Formalising textbooks like this however are I think a very good alternative way to get UGs involved; my M1F explained repo (the name is an Imperial in joke) was very popular this summer with my project students, probably about 50% of them ended up contributing to it in one way or another (even if not all of them worked out how to do PRs -- people were emailing me proofs etc).

[Moritz Firsching]

Very few proofs in that book are "pictures" or rely on geometric intuition.

Re having sorried-statements: that makes sense! I plan to go through some chapters and add more sorried statements/partial proofs.
I did already link to the open sorrys in the README.md:
https://github.com/mo271/formal_book/search?q=sorry+extension%3Alean
(Perhaps such a link would also be useful for https://github.com/ImperialCollegeLondon/m1fexplained?!)

[Moritz Firsching]

Yaël Dillies said:

docs#symm_diff_assoc is a proof from Proofs of the book.

Yeah, and there are a couple of other places where mathlib follows Proofs from the book closely, most notably the entire proof of Bertrand's postulate

[Bryan Gin-ge Chen]

Yaël Dillies said:

docs#symm_diff_assoc is a proof from Proofs of the book.

Hmm, I don't think that's true (unless the proof has been replaced since I added it). I believe the title and introduction of the reference linked in the module doc claim that the proof presented is a proof from "the Book" rather than claiming that it's a proof from "Proofs [from] the book".

[Junyan Xu]

I think the most conceptual proof uses the fact that the symmetric difference of two sets correspond to pointwise addition of their indicator functions taking value in zmod 2. This proof is not intuitionistic though.

[Bryan Gin-ge Chen]

symm_diff_assoc applies to (generalized) Boolean algebras though - is there a suitable notion of indicator function at that level of generality?

[Yaël Dillies]

I suspect that would need atomicity.

[Junyan Xu]

A generalized Boolean algebra embeds into a Boolean algebra according to https://math.stackexchange.com/a/2985310/12932, and a Boolean algebra embeds into a powerset algebra by Stone's representation theorem. These should be enough to reduce the problem to powerset algebras.

(Hmm and I think the original proof can't be made intuitionistic either; some double negation is involved. Not sure if the co-Heyting diff works, or whether using ¬(p ↔ q) or ¬(p → q) ∨ ¬(q → p) to define symm_diff makes any difference.)

[Yaël Dillies]

If it could be made intuitionistic, it would hold in co-Heyting algebras, and the dual would hold in Heyting algebras, but the following fails:

lemma iff_assoc {p q r : Prop} : (p ↔ (q ↔ r)) ↔ ((p ↔ q) ↔ r) := by itauto -- fails

[Bolton Bailey]

OP might be interested to know, the proof of Bertrand’s postulate now in mathlib follows the approach of Aigner and Ziegler

[Bolton Bailey]

(Actually I see someone already commented this)

[Junyan Xu]

Yaël Dillies said:

If it could be made intuitionistic, it would hold in co-Heyting algebras, and the dual would hold in Heyting algebras, but the following fails:

lemma iff_assoc {p q r : Prop} : (p ↔ (q ↔ r)) ↔ ((p ↔ q) ↔ r) := by itauto -- fails

Indeed, one comment here pointed out associativity is equivalent to the law of excluded middle.

[Mario Carneiro]

not sure about equivalent to LEM, but it's certainly not intuitionistically true

[Junyan Xu]

The last comment below the answer shows it's equivelent to double negation elimination, which is equivalent to LEM. Here's a Lean proof:

import tactic
def iff_assoc : Prop := ∀ (p q r : Prop), ((p ↔ q) ↔ r) ↔ (p ↔ (q ↔ r))
def lem : Prop := ∀ (p : Prop), p ∨ ¬p

lemma iff_assoc_iff_lem : iff_assoc ↔ lem :=
begin
  split; intro h,
  { have : ∀ p, ¬¬p → p := λ p, ((h p false ¬p).1 $ iff_false p).2 ∘ (false_iff ¬p).2,
    exact λ p, this _ (λ n, n $ or.inr $ n ∘ or.inl) },
  { intros p q r, cases h p; cases h q; cases h r; revert h_1 h_2 h_3; itauto },
end

#print axioms iff_assoc_iff_lem /- no axioms -/