General

Stream: Proofs from the book

[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. So we should't expect it (and the dual symm_diff version) to hold outside of (generalized) boolean algebras.

[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 -/

[Moritz Firsching]

By now, we have added a blueprint for the Proofs from the BOOK repo! (thanks @Patrick Massot for making the blueprint repo and to @Pietro Monticone for helping me setting it up, after an earlier non-successfull attempt):

The dependency graph is quite wide, because there is little inter-dependency between the chapters.

I hope adding the blueprint will make it easier to contribute and work together! There are still lots of easy sorrys statements / proofs that should be relatively simple to formalize, but also more involved stuff, so contributions from beginners as well as experts are most welcome.

[Ruben Van de Velde]

There's a latex error in https://firsching.ch/FormalBook/blueprint/sect0008.html#book.irrational.Theorem_3

[Riccardo Brasca]

@Luigi Massacci should have somewhere a formalization of the topological proof of the infinitude of the primes.

[Moritz Firsching]

Ruben Van de Velde said:

There's a latex error in https://firsching.ch/FormalBook/blueprint/sect0008.html#book.irrational.Theorem_3

Thanks, will fix, looks like colonequals is not supported...

[Yaël Dillies]

Did you ever get the formalisations from @Yves Jäckle ?

[Yaël Dillies]

If not, I'll swallow them into LeanCamCombi so that they are on the PR treadmill

[Michael Stoll]

The sixth proof of the infinitude of primes is in Mathlib: not_summable_one_div_on_primes and Nat.Primes.not_summable_one_div.

[Moritz Firsching]

Yaël Dillies said:

Did you ever get the formalisations from Yves Jäckle ?

No, not yet, but thanks for the pointer!

[Kevin Buzzard]

If we know that $L(1,\chi)$ is some rational multiple of $\pi$ where $\chi$ is the level 4 Dirichlet character (it's $\pi/4$ isn't it?), then we could get another proof coming from the product formula and the now-proved fact that $\pi$ is irrational! If there were only finitely many primes then the product would be finite.

[Yves Jäckle]

FYI, I'm currently still working on a different formalization project, which should hopefully be done by the end of this year. Then, my plan was to add some finite geometry API to mathlib so that I can finish the graph theory proof in the chapter on the pigeonhole principle and double counting (and also clean that proof :sweat_smile: ). I'm fine with my code being shared, and hope we can collaborate :+1:
@Christoph Spiegel

[Christoph Spiegel]

Just to note: I have started a similar project at https://github.com/FordUniver/thebook.lean, which I am currently trying to revive after a period of dormancy. I don't think there's anything in there that isn't already covered by the work of @Moritz Firsching or @Yves Jäckle.

I believe it makes sense for these projects to remain somewhat disjoint, aside from perhaps occasionally pulling code from one repository to another, because of some key differences:

• It is primarily intended as the code basis underlying the blog thebook.zib.de.
• I don't plan to limit myself to content from Aigner and Ziegler; it's just a good initial resource.
• The proofs are intended to follow the written human versions as closely as possible and therefore, the code style is perhaps also somewhat particular and not to everyone's liking.

Basically I think of it as a sort of Rosetta stone intended for mathematicians not familiar with lean. Nevertheless, should anyone be interesting in joining and writing some proof with a matching post, I'd be more than happy about that!

[Moritz Firsching]

@Christoph Spiegel good to know, thanks for the heads up! Looks like it might indeed be useful to sometimes borrow code from each other, and I agree that we have slightly different goals here, as you describe!

[Luigi Massacci]

I'll PR Fürstenberg's proof as soon as I'm done with midterms (so in two weeks)

[Christoph Spiegel]

I now have a functioning version of the CS proof of Mantel's theorem: https://github.com/FordUniver/thebook.lean/blob/main/TheBook/GraphTheory/Mantel/CauchyInequality.lean

@Moritz Firsching do you already have this or should I PR?

[Moritz Firsching]

Nice, I don't, please do pr it!

[Christoph Spiegel]

Will do! I should mention though that it‘s currently only the upper bound on the number of edges, not characterizing evenly split complete bipartite graphs as the only extremal constructions

[Moritz Firsching]

Still great!

[Miguel Marco]

One question: the idea for this project is just to prove the statements in the book in Lean, or to do so following the actual proofs in the book?

In other words: are we aiming at creating Lean proofs or at translating proofs to Lean?

[Moritz Firsching]

Good question: The idea is much more on the translating the proofs to Lean proofs. There are even a few chapter with 5 or 6 different proofs for the same statement: for those the plan is to formalize all of them. How close it is possible to follow while maintaining at least somewhat idomatic Lean code is to some degree a matter of taste, but the at least the ideas of the proofs should be reflected in the Lean proofs.

[Christoph Spiegel]

I also have a proof of the handshaking lemma that follows the blackboard argument a bit more closely than the mathlib proof does: https://thebook.zib.de/graph%20theory/2024/10/11/handshaking-lemma.html

@Moritz Firsching stuff that is in current PRs presumably goes into the Mathlib folder?

[Moritz Firsching]

Great!

Yes, let's make an ForMathlib folder for those!

[Christoph Spiegel]

@Moritz Firsching are you basing it on revision 4 or 5 of the book?

[Moritz Firsching]

I'm using the sixth (lastest) edition

[Christoph Spiegel]

Ah right sixth was the latest

[Christoph Spiegel]

That's good because that's what I'm also on and I think the chapters changed from 5 to 6

[Yao Liu]

i wonder if Lean is good at detecting hidden circular argument, if there is one. Do you really prove stuff about Dirchlet series without using infinitude of primes?

[Moritz Firsching]

I think some human assistance might be needed. At least some AI seemed to have trouble with that: using Field.toIsField to prove Wedderburn, see https://github.com/mo271/FormalBook/pull/67. Another example of the failure here is that Proofs from the book often has more than proofs of the same result. I tried to model this

theorem result_1 [statement] := by
[proof 1]

theorem result_2 [same statement] := by
[proof 2]

Apparently LeanAgent then idea to prove

theorem result_2 := by result_1

which of course would also have been found by exact?
I'm not sure if there is a better way to go about these "multiple proofs for the same statement" problem.

[Moritz Firsching]

I added the second proof in "Chapter 4: Representing numbers as sums of two squares". (Still contains some sorrys!)
This is the one by Heath-Brown, on which Zagier's one-sentence version is based on. I follow the structure of proof of this formalized by @Jeremy Tan and @Thomas Browning.
Since the latest edition of Proofs from THE BOOK also has the illustration with "windmills", I added a widget that draws the windmill corresponding to a given triple (x, y, z) and then one can also get it to draw the other triple in that involution. It takes as argument colors?, so one can easily only focus on the shape which will be the same for two triples mapped to each other under the involution.
Here's a link to an animation of how the widget looks like: https://gist.github.com/mo271/162c127fb6f6ee382df245e773a2b365
You can of course also try it out directly from the FormalBook repo:  https://github.com/mo271/FormalBook

[Kevin Buzzard]

There was a recent formalisation of the windmills approach in Coq which made it into either ITP or CPP IIRC.

[Dhyan Aranha]

Hi all, we are running a lean learning seminar here at the University of Amsterdam and our group would like to work on formalizing things from "proofs from the book". I was wondering if it would be possible to have a separate channel for us to discuss/work collaboratively?

[Johan Commelin]

I'll set things up for you.

[Dhyan Aranha]

[Quoting…]

thanks!

[Johan Commelin]

Voila #Proofs from the book

[Luigi Massacci]

@Moritz Firsching I’ve PR-ed Furstenberg’s proof of infinitude of primes, if you have any improvements you’d like to suggest I promise I’ll implement them promptly. I was stopped by the bot and signed google’s licensing agreement, not sure what’s supposed to happen now…

Regardless, I’ve noticed that the text of the blueprint is word for word the text of the actual book, and while Springer’s IP rights are infinitely low down the list of my personal concerns, I imagine they might not be too happy about this, or was the book released on a CC license?

[Moritz Firsching]

Can somebody who has the permission move this message (or the entire topic) to the new Proofs From the Book channel?

[Moritz Firsching]

Thanks looks great, will reply on the pr

[Notification Bot]

This topic was moved here from #general > Proofs from the book by Riccardo Brasca.

[Riccardo Brasca]

Moritz Firsching said:

Can somebody who has the permission move this message (or the entire topic) to the new Proofs From the Book channel?

Done. The title should probably be changed.

[Moritz Firsching]

Thanks, I tried to change the title to "General", but don't have permission for this. (Only the last 9 out of 46 messages would be moved with my permissions...)

[Riccardo Brasca]

Title changed.