## Stream: condensed mathematics

### Topic: for_mathlib

#### Kevin Buzzard (Feb 05 2021 at 17:55):

OK so we're not quite at lean-perfectoid-space levels yet,but with 14 files in for_mathlib we are beginning to walk into the same trap which Johan, Patrick and I walked into in 2019, generating a whole bunch of stuff which was _clearly_ for mathlib, much of it even mathlib-ready, and then not PR'ing it and then it rotted and the work we put in there was, arguably, wasted (although of course it fulfilled the role of helping us formalise perfectoid spaces). Do we have a plan here, or are we just going to watch this directory fill up and then go "oh look it happened again"? There are over 1300 lines of code in that directory so far.

#### Patrick Massot (Feb 05 2021 at 17:57):

My opinion is we should explicitly state that everything in the folder can be PRed to mathlib by anyone. If it means someone feel they lose credit then it means they should have made the PRing effort. Of course when things do not get PRed then the author should still be the only one to feel bad.

#### Johan Commelin (Feb 05 2021 at 18:03):

yes, I very much agree with what Patrick said.

#### Kevin Buzzard (Feb 05 2021 at 18:03):

I personally never feel that it is about "credit". However when I was making the universal_universe branch on this repo I didn't put anything in for_mathlib, I just made notes of what needed to be PR'ed and am slowly PR'ing it myself. I did the same today. I think there is a risk that nobody does it. Of course anyone can feel free to do it, but we all know it's hard work. I am wondering if we need a better plan than this. Or do you think I'm overreacting and it doesn't matter?

Chris Hughes has long argued that free_abelian_group should be defined via finsupp. I see now that Johan has just made the interface relating the current definition to finsupp. Chris won't be happy because he wanted the equality to be definitional, but I am less excited by definitional equality than he is. This is 300 lines of code though. It probably should not be lost!

#### Johan Commelin (Feb 05 2021 at 18:10):

I agree that we should work on PRing things. But on the other hand, momentum is also a weird concept... once I have momentum working on a project like this, I just want to march forward, and not be blocked by PRs.

#### Johan Commelin (Feb 05 2021 at 18:10):

Something I would like to experiment with, is whether we can do some sort of for_mathlib PR sprints.

#### Johan Commelin (Feb 05 2021 at 18:11):

Once we reach some sort of intermediate milestone/target, we just take a step back, and create 37 PRs to mathlib. And after that we plunge forward to the next target.

#### Kevin Buzzard (Feb 05 2021 at 18:27):

Johan this is exactly how I felt with perfectoid. Once I could see that it was possible to do this kind of mathematics in Lean (because in 2018 this was not yet clear, as you well remember!), I would just throw myself into a lot of focussed coding with clear well-defined goals in mind and fill up for_mathlib and just not worry. All three of us were doing it, and then Patrick suddenly saw sense and PR'd a whole bunch of topology into mathlib (all the Bourbaki stuff which he'd done) -- but I can't remember whether this was during the sprint to the def or after we had the def.

#### Patrick Massot (Feb 05 2021 at 18:47):

It was during the sprint, but there was a special trick. mathlib had stuff about this, but it wasn't good enough and was actually getting in our way. That's why I was force to work on the mathlib side.

#### Scott Morrison (Feb 05 2021 at 22:29):

I'm glad there's consensus that "anyone should feel free to make the PRs from for_mathlib". This is a chore that I don't find particularly tedious, and will make some effort at it after the weekend!

#### Johan Commelin (Feb 10 2021 at 12:46):

Anyone looking for some PRs to make:

\$ find src/for_mathlib/ -name '*.lean' | xargs wc -l
189 src/for_mathlib/sequences.lean
21 src/for_mathlib/category_theory.lean
34 src/for_mathlib/tsum.lean
31 src/for_mathlib/extend_from_nat.lean
403 src/for_mathlib/normed_group_hom.lean
55 src/for_mathlib/equalizers.lean
114 src/for_mathlib/topology.lean
18 src/for_mathlib/linear_algebra.lean
19 src/for_mathlib/topological_group.lean
62 src/for_mathlib/locally_constant.lean
362 src/for_mathlib/free_abelian_group.lean
40 src/for_mathlib/compact.lean
1440 total


#### Johan Commelin (Feb 10 2021 at 12:47):

I think I'll take on free_abelian_group and locally_constant

#### Riccardo Brasca (Feb 10 2021 at 12:50):

I can do sequences

#### Riccardo Brasca (Feb 10 2021 at 12:55):

Ops, it depends on locally_constant, it is better to wait.

#### Kevin Buzzard (Feb 10 2021 at 13:52):

I made a PR to free_abelian_group recently, which came out of the universal maps stuff. #6062. It's waiting for epsilon more work by me.

#### Johan Commelin (Feb 10 2021 at 21:37):

I ended up working on for_mathlib/compact first...

#### Johan Commelin (Feb 10 2021 at 21:37):

I hope to tackle locally_constant asap

#### Johan Commelin (Feb 11 2021 at 21:47):

for_mathlib/locally_constant has now been PRd

#### Johan Commelin (Feb 23 2021 at 08:45):

#6375 PRs most of normed_group_hom to mathlib. About 20% of for_mathlib (-;

#### Johan Commelin (Mar 10 2021 at 06:38):

This PR has now been merged, and so ~370 lines of for_mathlib were deleted this morning.

#### Johan Commelin (Mar 10 2021 at 06:38):

Be sure to git pull before you work on master

#### Johan Commelin (Mar 10 2021 at 06:39):

What is left:

  185 src/for_mathlib/sequences.lean
34 src/for_mathlib/tsum.lean
31 src/for_mathlib/extend_from_nat.lean
55 src/for_mathlib/equalizers.lean
114 src/for_mathlib/topology.lean
14 src/for_mathlib/pi_nat_apply.lean
18 src/for_mathlib/linear_algebra.lean
19 src/for_mathlib/topological_group.lean
362 src/for_mathlib/free_abelian_group.lean
319 src/for_mathlib/normed_group_quotient.lean