## Stream: graph theory

### Topic: freek 83

#### Jalex Stark (Aug 15 2020 at 13:21):

I started down the "PR graph theory to lean" path when Aaron came to me with a mostly-error-free proof of the "friendship theorem" which characterizes graphs with the property "every pair of distinct vertices has a unique common neighbor". We used some algebraic stuff in our proof, which has since been sliced up and PRed, except for the coupld of most specialized lemmas.

#### Jalex Stark (Aug 15 2020 at 13:23):

The branch is here
https://github.com/leanprover-community/mathlib/tree/freek_83_friendship_theorem
(the code is in the archive / 100-theorems folder)

#### Jalex Stark (Aug 15 2020 at 13:24):

It needs quite a bit more polishing. It may also be a good testbed for changes to the API.

#### Jalex Stark (Aug 15 2020 at 13:25):

There's a nontrivial counting argument there, with some machinery that maybe one could profitably re-use elsewhere.

#### Jalex Stark (Aug 24 2020 at 23:25):

#3458 was born from this project, and now it's approved. I think @Aaron Anderson plans to slice off the rest of branch#freek_83_friendship_theorem into PRs; possibly the PRs don't need to depend on each other very much.

#### Aaron Anderson (Aug 24 2020 at 23:28):

One of those PRs has already been PR'd, the one on adjacency matrices #3672

#### Jalex Stark (Aug 24 2020 at 23:29):

sorry I don't see a PR on #3672. did you mean to say "approved"?

#### Kyle Miller (Aug 24 2020 at 23:29):

To save you a little work: mul_val is now known as mul_apply in the newest mathlib

#### Aaron Anderson (Aug 24 2020 at 23:30):

Jalex Stark said:

sorry I don't see a PR on #3672. did you mean to say "approved"?

I just mean that I've created the PR.

#### Jalex Stark (Aug 24 2020 at 23:32):

got it. a PR is just a branch of mathlib + a request to merge that branch into master. Someone who doesn't have push access to branches of mathlib could hypothetically open a pull request to merge stuff into an open PR, the same way that you can push stuff to the PR branch.

#### Jalex Stark (Aug 24 2020 at 23:32):

and this PRing a PR is not just hypothetical, sometime this summer a new contributor opened a PR on a PR, thinking it was a PR to master, then we ended up in a state where both PRs were reviewed and marked as approved, but neither of them got merged into master

#### Kyle Miller (Aug 24 2020 at 23:34):

I was surprised GitHub does PRs based on a branch rather than a commit. It makes some sense, because it makes it easier to incorporate code review changes, but, still, it causes problems like what you describe.

#### Aaron Anderson (Aug 24 2020 at 23:49):

IIRC the remaining work breaks into (adjacency matrix PR) and (friendship proof + like 2 linear algebra lemmas PR)

#### Aaron Anderson (Aug 24 2020 at 23:50):

maybe that second one is too big, but I don't remember any sensible ways to break it up

#### Aaron Anderson (Aug 27 2020 at 00:27):

Check out branch#friendship_final

#### Aaron Anderson (Aug 27 2020 at 00:29):

I've placed the prerequisites around the library. Feel free to give me comments here, or edit or golf.

#### Aaron Anderson (Aug 27 2020 at 00:34):

I'm going to PR all the prereqs not in the one archive file separately first

#3953

#### Jalex Stark (Aug 27 2020 at 00:53):

Aaron Anderson said:

Check out branch#friendship_final

are we ready to delete the freek_83_friendship_theorem branch?

#### Aaron Anderson (Aug 27 2020 at 00:56):

I think there’s extra stuff on there, like a slightly different approach to adjacency matrix generalization.

#### Aaron Anderson (Aug 27 2020 at 00:57):

I should double-check that everything I want is backed up and get back to you tonight.

#### Jalex Stark (Aug 27 2020 at 01:00):

No rush. Now that I think of it, I have an old mathlib branch (I had worked just a bit on freek 73 before Bhavik PRed it) to garbage-collect.

#### Aaron Anderson (Aug 27 2020 at 03:18):

You can delete it now.

#### Aaron Anderson (Aug 27 2020 at 03:19):

branch#friendship_final builds, although it'll stay unlinted until I merge the prereqs branch back in

#### Kyle Miller (Aug 27 2020 at 06:30):

Aaron Anderson said:

Feel free to give me comments here, or edit or golf.

I've pushed a few commits for the friendship lemma. It changes some definitions, splits off a lemma or two, and adds some documentation. (If any of the changes aren't welcome, feel free to revert.)

#### Aaron Anderson (Aug 27 2020 at 07:18):

That all looks good to me, but I should probably review it again tomorrow.

#### Aaron Anderson (Aug 29 2020 at 02:16):

The prereqs PR hasn't been merged yet, but it's far enough along that I'm comfortable creating #3970

#### Jalex Stark (Aug 29 2020 at 13:56):

ah, the diff looks very beefy, but that's just because it has the diff from the unmerged prereqs PR

#### Aaron Anderson (Aug 29 2020 at 17:23):

#3953 is on the merge queue, and when it merges, there should only be one file in the diff

#### Aaron Anderson (Aug 29 2020 at 18:56):

It merged, there is now only one file in the diff

Last updated: May 08 2021 at 22:13 UTC