[Merged by Bors] - feat(archive/100-theorems-list): friendship theorem (nr 83) #3970

awainverse · 2020-08-29T02:13:28Z

defines friendship graphs
proves the friendship theorem (freek #83)

…prover-community/mathlib into freek_83_friendship_theorem

…_theorem

semorrison · 2020-09-01T00:28:34Z

archive/100-theorems-list/83_friendship_graphs.lean

+- The friendship theorem (Erdős, Rényi, Sós 1966) states that every finite friendship graph has a
+  politician.


Could you give a full reference to the paper?

Is their proof the one you are formalising? If not, can you add references to what you are following?

I've provided a link to the paper in question, and the paper with the proof that's closest to what we used. I'm going to have to figure out the standard format for full references.

I think this is the right bibtex and all?

archive/100-theorems-list/83_friendship_graphs.lean

semorrison · 2020-09-01T00:34:18Z

Looks nice!

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

jcommelin

Thanks!

jcommelin · 2020-09-01T03:59:08Z

archive/100-theorems-list/83_friendship_graphs.lean

+
+/-- If `d ≤ 1`, a `d`-regular friendship graph has at most one vertex, which is
+  trivially a politician. -/
+lemma deg_le_one_friendship_has_pol (hd : G.is_regular_of_degree d) (hd1 : d ≤ 1) :


Suggested change

lemma deg_le_one_friendship_has_pol (hd : G.is_regular_of_degree d) (hd1 : d ≤ 1) :

lemma exists_politician_of_degree_le_one (hd : G.is_regular_of_degree d) (hd1 : d ≤ 1) :

I think a lot of names here could be updated to the mathlib style guide. Of course this is the archive, and not mathlib-proper. But on the other hand, you could view this as an opportunity to showcase "how it's done".

In a similar spirit, I think some of the docstrings could be improved a bit, so that they are clear, even when read out of context.

Oof, sorry for not going through those, wrote those months ago, so it all looked normal to me by now.
It should be a lot better now, although most names are a little longer.

@awainverse Would you please also rewrite some of the docstrings a bit, like I wrote in the second half of the post upstairs?

Yes, sorry.

I think the docstrings are a little more clear. If this doesn't look good, could you give me an example of a docstring that isn't clear on its own?

jcommelin · 2020-09-01T04:00:08Z

archive/100-theorems-list/83_friendship_graphs.lean

+/-- We know that a friendship graph has a politician or is regular, so we assume it's regular.
+  If the degree is at most 2, we observe by casework that it has a politician anyway.
+  If the degree is at least 3, the graph cannot exist. -/
+theorem friendship_theorem : exists_politician G :=


Btw, I'm ok with keeping this name as it is. 😄

jcommelin · 2020-09-01T05:55:57Z

Please rewrite the docstrings a bit, so that they make sense out of context. Once that is done, this looks good to me!

jcommelin

Thanks 🎉

bors merge

defines friendship graphs proves the friendship theorem (freek #83) Co-authored-by: Aaron Anderson <awainverse@gmail.com>

bors · 2020-09-01T07:23:49Z

Pull request successfully merged into master.

Build succeeded:

defines friendship graphs proves the friendship theorem (freek #83) Co-authored-by: Aaron Anderson <awainverse@gmail.com>

jalex-stark and others added 30 commits July 18, 2020 17:55

init

3b3c9ea

remove extra file

8ea8b3f

variables in sym_matrix

2ec56b8

imports, friendship

44c2cd9

fixed broken proof

ad8dca8

Hopefully updating char_poly.lean enough

ee39e24

golf

5ccdfe3

remove unnecessary line

840648c

Merge branch 'freek_83_friendship_theorem' of https://github.com/lean…

a97aaef

…prover-community/mathlib into freek_83_friendship_theorem

import golf

5c7502f

renaming

f129ef8

clean proofs

4245a85

separate simple_graph

61e16b5

golf

4db1f66

rename

7e4e3a2

..and remove the old file

101bf55

golf

11168ae

golf

c07106d

optimize main proof

1b3ba82

unified pows

d5e13ba

golf

167a887

Merge remote-tracking branch 'origin/master' into freek_83_friendship…

0de44e6

…_theorem

formatting

9e09caf

golf

bfdad05

golf

3fd630f

copyright

b28cf1c

explicit arguments

f95f4e8

formatting

13fb06a

Kyle's graph nomenclature

aac328a

Edge set

d213dc6

Reviews

2bfb784

awainverse added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Aug 31, 2020

semorrison reviewed Sep 1, 2020

View reviewed changes

archive/100-theorems-list/83_friendship_graphs.lean Outdated Show resolved Hide resolved

awainverse and others added 3 commits August 31, 2020 17:52

a politician

7bd1765

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

References

e607e65

Better references

5f856b4

jcommelin requested changes Sep 1, 2020

View reviewed changes

jcommelin added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Sep 1, 2020

Renaming lemmas

b3d14f2

awainverse added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Sep 1, 2020

jcommelin added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Sep 1, 2020

Editing docstrings

5533707

awainverse added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Sep 1, 2020

jcommelin approved these changes Sep 1, 2020

View reviewed changes

github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Sep 1, 2020

bors bot pushed a commit that referenced this pull request Sep 1, 2020

feat(archive/100-theorems-list): friendship theorem (nr 83) (#3970)

2688d42

defines friendship graphs proves the friendship theorem (freek #83) Co-authored-by: Aaron Anderson <awainverse@gmail.com>

bors bot changed the title ~~feat(archive/100-theorems-list): friendship theorem (nr 83)~~ [Merged by Bors] - feat(archive/100-theorems-list): friendship theorem (nr 83) Sep 1, 2020

bors bot closed this Sep 1, 2020

bors bot deleted the friendship_final branch September 1, 2020 07:23

PatrickMassot pushed a commit that referenced this pull request Sep 8, 2020

feat(archive/100-theorems-list): friendship theorem (nr 83) (#3970)

58e0170

defines friendship graphs proves the friendship theorem (freek #83) Co-authored-by: Aaron Anderson <awainverse@gmail.com>

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(archive/100-theorems-list): friendship theorem (nr 83) #3970

[Merged by Bors] - feat(archive/100-theorems-list): friendship theorem (nr 83) #3970

awainverse commented Aug 29, 2020

semorrison Sep 1, 2020

awainverse Sep 1, 2020

awainverse Sep 1, 2020

semorrison commented Sep 1, 2020

jcommelin left a comment

jcommelin Sep 1, 2020

awainverse Sep 1, 2020

jcommelin Sep 1, 2020

jcommelin Sep 1, 2020

awainverse Sep 1, 2020

awainverse Sep 1, 2020

jcommelin Sep 1, 2020

jcommelin commented Sep 1, 2020

jcommelin left a comment

bors bot commented Sep 1, 2020

		- The friendship theorem (Erdős, Rényi, Sós 1966) states that every finite friendship graph has a
		politician.

	lemma deg_le_one_friendship_has_pol (hd : G.is_regular_of_degree d) (hd1 : d ≤ 1) :
	lemma exists_politician_of_degree_le_one (hd : G.is_regular_of_degree d) (hd1 : d ≤ 1) :

[Merged by Bors] - feat(archive/100-theorems-list): friendship theorem (nr 83) #3970

[Merged by Bors] - feat(archive/100-theorems-list): friendship theorem (nr 83) #3970

Conversation

awainverse commented Aug 29, 2020

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

semorrison commented Sep 1, 2020

jcommelin left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

jcommelin commented Sep 1, 2020

jcommelin left a comment

Choose a reason for hiding this comment

bors bot commented Sep 1, 2020