## Stream: new members

### Topic: Contributing to mathlib

#### Stuart Presnell (Nov 01 2021 at 20:25):

Hi, I'm interested in contributing to mathlib, so I'd like to start with some extremely simple PRs just to check I understand how the process works (as explained in the "Making a pull request" video). My github user name is stuart-presnell. Could someone grant me the required access?

#### Stuart Presnell (Nov 01 2021 at 20:35):

Great, thank you!

#### Scott Morrison (Nov 01 2021 at 20:54):

Welcome, @Stuart Presnell! Do you have ideas of things you'd like to work on?

#### Stuart Presnell (Nov 01 2021 at 21:06):

I'd like to be able to work on some analytic number theory, but that will take a while. In the near term, I was thinking of adding some very simple utility lemmas on integers and lists.

#### Stuart Presnell (Nov 01 2021 at 21:12):

I'm working from the principle that anything that's 'obvious' should be solvable automatically, so I'm writing lemmas that handle obvious steps that I can't figure out how to get Lean to fill in. Does that seem like a reasonable approach?

#### Kevin Buzzard (Nov 01 2021 at 21:20):

Sure! If you PR those lemmas you might find that some members of the community will try to golf them -- the general principle for mathlib seems to be that if it's mathemtically trivial then the proof in the library should be as concise as possible, and hang readability.

#### Kevin Buzzard (Nov 01 2021 at 21:23):

Warning: I would also like to work on some analytic number theory, but this is blocked by the current state of complex analysis; right now we don't have much API for integrals over complex contours, so we don't have the result that a uniform limit of holomorphic functions is holomorphic, so we can't prove that the Riemann zeta function is holomorphic yet (unless we go around the houses and give a bespoke proof, which is not the mathlib way; not being the mathlib way is also the reason why we don't have much API for single variable complex integration)

#### Stuart Presnell (Nov 01 2021 at 21:36):

Is there a list of the 'this is obvious, solve it for me' tactics? I know about some of the more obvious ones like library_search, tauto, and omega, but it would be good to have a more comprehensive list so I'm not trying to prove something that Lean can already solve.

#### Stuart Presnell (Nov 01 2021 at 21:38):

Oh, and my knowledge and ambitions in analytic number theory are much more modest at the moment, so I'm not expecting to run into those limitations any time soon!

#### Alex J. Best (Nov 01 2021 at 21:43):

You could look at the things tagged decision procedure or finishing in the mathlib tactics list https://leanprover-community.github.io/mathlib_docs/tactics.html. I'd add tactic#finish and ofc tactic#refl to the list of things I try before giving up, and tactic#suggest when library search isn't finding a proof will often get you close, there are a few other good ones on the page like tactic#norm_cast, tactic#linarith and tactic#norm_num for more specialized situations but are very powerful when they apply

#### Alex J. Best (Nov 01 2021 at 21:46):

Note that omega is currently being phased out of mathlib itself, despite its usefulness it seems that having omega proofs will make porting to lean 4 harder as it is a large and complicated tactic, so we try and replace uses of omega by other things where possible

#### Kevin Buzzard (Nov 01 2021 at 22:04):

The complete list of tactics is a bit overwhelming at first, but for results within one area you usually figure out the important ones. simp is great once you've figured out what its domain is -- this took me a while

Thanks very much

#### Will Sawin (Nov 02 2021 at 03:50):

There's a lot of modern analytic number theory that doesn't really involve zeta functions, L-functions, or any other holomorphic functions in an essential way. For example work in the circle method or on sieves.

#### Kevin Buzzard (Nov 02 2021 at 06:53):

I really don't know much about this stuff at all. Helfgott's work on weak Goldbach springs to mind. It's a highly refined circle method which shows all odd numbers >= 10^30 or so are the sum of three primes and then a brute force calculation using I think C or C++ to deal with the rather large finite number of exceptions. This would be ridiculously hard to do in a theorem prover right now but on the other hand Ben Green did raise it with me once as something which involved a lot of fiddly estimates and would be worth checking in a theorem prover

#### Johan Commelin (Nov 02 2021 at 07:40):

The 10^30 definitely sounds like a job for Lean 4 instead of Lean 3 (-;

Or Coq

#### Kevin Buzzard (Nov 02 2021 at 08:46):

For something as simple as this one could imagine a two-prover effort

#### Kevin Buzzard (Nov 02 2021 at 08:47):

Or maybe it would be interesting to try the brute force computation part in both

#### Stuart Presnell (Nov 02 2021 at 10:38):

Alex J. Best said:

Note that omega is currently being phased out of mathlib itself, despite its usefulness it seems that having omega proofs will make porting to lean 4 harder as it is a large and complicated tactic, so we try and replace uses of omega by other things where possible

Is there a standard recommenced replacement for omega? Also, is there a way to add a note or warning about this to the relevant section of the mathlib tactics page so that newcomers know to avoid it?

#### Johan Commelin (Nov 02 2021 at 10:45):

@Stuart Presnell The replacement we are all hoping and longing for is "omega in Lean 4 as soon as mathlib is ported"

#### Eric Wieser (Nov 02 2021 at 10:51):

I don't think omega is a problem for newcomers to lean; only a problem for when those newcomers want to contribute to mathlib

#### Alex J. Best (Nov 02 2021 at 10:56):

Yeah I use omega all the time still when I'm working on stuff. Depending on what the goal is you might be able to use using tactic#zify to transfer the goal to a result about ints and then some other tactics can help.

#### Eric Wieser (Nov 02 2021 at 11:02):

There are lots of tactics which are great for rushing through a proof (ie non-terminal simp and tidy), and then should be removed after cleaning up for mathlib

#### Patrick Massot (Nov 02 2021 at 12:45):

Note that in an ideal world omega wouldn't be a forbidden tactic. The issue here is that the author lost interest in maintaining this tactic. It has bugs and very little documentation. And there is very little motivation to fix this in Lean 3. But we very much hope mathlib will have an analogue tactic (without bugs and with documentation) in Lean 4.

#### Mario Carneiro (Nov 02 2021 at 12:54):

If we eventually get a replacement for omega in lean 4 (and FYI I'm looking into this, nothing concrete to announce yet), then it will not be necessary to deprecate it in lean 3, since we can map the tactic to its replacement, even if it isn't a perfect match; the other lean 4 tactics are already not exact carbon copies anyway so it's fine if it's close enough and we fix the outliers

#### Kevin Buzzard (Nov 02 2021 at 13:40):

I genuinely hope it's not a perfect match in this case!

#### Will Sawin (Nov 02 2021 at 14:44):

Unfortunately Helfgott's weak Goldbach proof uses the Riemann zeta function. (In fact, it uses the claim that the first 10^13 zeroes of the Riemann zeta function lie on the critical line). I was thinking about applications of the circle method to Diophantine equations, not involving primes, as in the work of Birch or Waring's problem. I think zeta and L-functions are not used here, or at least not used in every result. I certainly don't know a replacement for weak Goldbach as something people are not 100% sure of the correctness of and would like checked down this line, but if someone just wants to contribute there should be lots available.

#### Will Sawin (Nov 02 2021 at 15:00):

Although maybe someone could work on things needed for Helfgott's proof while the zeta function is in development...

#### Patrick Massot (Nov 02 2021 at 15:02):

Note also that Coq checked some of the numerical integrals entering this work: https://hal.inria.fr/hal-01630143v2 They found errors but no critical ones.

#### Loreno Heer (Nov 30 2021 at 12:40):

Hi all,
I am learning lean 4 and looking for ways to contribute to mathlib or lean 4 itself. Where should I start?

#### Huỳnh Trần Khanh (Nov 30 2021 at 12:44):

oh? contributing to lean 4 probably isn't a good idea because you need lots of background knowledge and an understanding of the existing codebase... anyway you should contribute to mathlib instead, the barrier to entry is much lower

#### Huỳnh Trần Khanh (Nov 30 2021 at 12:45):

from what I gathered, one way to contribute to mathlib is to spawn a new project and formalize exciting theorems and stuff, and then make a topic on here to request your code to be included in mathlib

#### Johan Commelin (Nov 30 2021 at 12:47):

@Loreno Heer Currently, mathlib is using Lean 3. But several people are in the middle of a complicated semi-automated port to Lean 4. We hope that this "mathport" will be finished a couple of months from now.

#### Vincent Beffara (Jan 19 2022 at 18:24):

Hi, I formalized a few things in graph theory (Cayley graphs, contractions, minors, things like that) and would like to contribute them to mathlib. Could someone please grant me the rights to to PRs?

My handle on github is vbeffara (and my code is at https://github.com/vbeffara/lean but it needs a lot of refactoring before I submit most of if ...)

#### Patrick Massot (Jan 19 2022 at 18:26):

Done (with great pleasure!).

Thanks!

#### Jeoff Lee (Jan 24 2022 at 05:47):

Hi, I'm an undergrad interested in theoretical physics and computer science. I'm currently experimenting with formalizing theorems and making a pull request to mathlib. (https://github.com/null-lambda/mathlib/blob/master/archive/100-theorems-list/37_solution_of_cubic.lean)
Could someone give me the required access?

#### Johan Commelin (Jan 24 2022 at 06:02):

Looks like you have access now, right?

#### Johan Commelin (Jan 24 2022 at 06:04):

@Jeoff Lee Aah, I see that you opened a PR from your fork. Well, here's an invitation for write access to non-master branches of mathlib: https://github.com/leanprover-community/mathlib/invitations

Thanks a lot!

#### Ella Yu (Dec 01 2022 at 01:07):

Hi, I am Ella Yu with github user name: KeYu-Ella. I have collaborated with Yaël Dillies to work on defining additive energy, and I wish to have access so that I can add myself as a co-author. Could someone grant me access please? Thanks a lot!

#### Aleksandar Milchev (Dec 12 2022 at 17:58):

Hello! I am a new user and I would like to contribute to the library by implementing a proof for the Max-Flow Min-Cut theorem for flow networks. How should I do that? Is there someone else, who is working on that and if yes, how should I approach the implementation of the proof in that case?
I am also new to lean and all materials that can be helpful (or relevant to the topic) will be much appreciated.

#### Yuyang Zhao (Dec 12 2022 at 19:26):

I think we don't even have a definition of networks now, but we have several definitions of graphs.

#### Martin Dvořák (Dec 12 2022 at 19:30):

Aleksandar Milchev said:

Hello! I am a new user and I would like to contribute to the library by implementing a proof for the Max-Flow Min-Cut theorem for flow networks. How should I do that? Is there someone else, who is working on that and if yes, how should I approach the implementation of the proof in that case?
I am also new to lean and all materials that can be helpful (or relevant to the topic) will be much appreciated.

In order to follow any of the classical proofs (you first have to prove that the Max-Flow exists), you will need to implement a Max-Flow algorithm in Lean first. This will require a non-trivial amount of functional programming. Do you have any experience with that?

#### Martin Dvořák (Dec 12 2022 at 19:38):

Are you going to prove it for rational capacities?

#### Aleksandar Milchev (Dec 12 2022 at 19:59):

Martin Dvořák said:

Aleksandar Milchev said:

Hello! I am a new user and I would like to contribute to the library by implementing a proof for the Max-Flow Min-Cut theorem for flow networks. How should I do that? Is there someone else, who is working on that and if yes, how should I approach the implementation of the proof in that case?
I am also new to lean and all materials that can be helpful (or relevant to the topic) will be much appreciated.

In order to follow any of the classical proofs (you first have to prove that the Max-Flow exists), you will need to implement a Max-Flow algorithm in Lean first. This will require a non-trivial amount of functional programming. Do you have any experience with that?

Yes, my idea is to prove it for rational capacities. As for functional programming, I have done a lot of practicals in Haskell and can say that I am confident in my skills with it, but that is my only functional programming experience.

#### Martin Dvořák (Dec 12 2022 at 20:12):

Great!! Programming in Lean is similar to programming in Haskell. I think you will like it.

#### Martin Dvořák (Dec 12 2022 at 20:16):

Let's first wait, however, for someone to give you advice about what you should base the definition of network flow on.

#### Yuyang Zhao (Dec 12 2022 at 20:34):

There are docs#quiver and indexed multigraphs in #16100. I think indexed multigraphs would be helpful (you may want reverse edges), but #16100 is still WIP. See also this topic

(edit: oops, another suggested definition in #16100 will not give you two arcs for each edge. I'm not sure which one we'll use eventually.)

#### Yaël Dillies (Dec 12 2022 at 20:41):

I'm getting back to #16100 sometimes this week :smile:

#### Yaël Dillies (Dec 12 2022 at 20:41):

Currently butchering the rest of my todo list.

#### Aleksandar Milchev (Dec 12 2022 at 21:22):

Yuyang Zhao said:

There are docs#quiver and indexed multigraphs in #16100. I think indexed multigraphs would be helpful (you may want reverse edges), but #16100 is still WIP. See also this topic

(edit: oops, another suggested definition in #16100 will not give you two arcs for each edge. I'm not sure which one we'll use eventually.)

I will definitely have a look (reversed edges will be useful), thank you!

#### Antoine Labelle (Dec 12 2022 at 21:32):

For undirected multigraphs, you can always use docs#quiver.has_involutive_reverse, which is relatively close to the definition proposed in #16100 but is already there in mathlib.

#### Antoine Labelle (Dec 12 2022 at 21:38):

I am adding some more API for quivers with graph theory in mind together with @Rémi Bottinelli (more precisely we want to get to covering maps of graphs and Cayley/Schreier graphs). The only thing about quivers is that dependant type subtleties quickly arise, so you have to be careful about that, but it's manageable using things in combinatorics.quiver.castand docs#heq.

#### Aleksandar Milchev (Dec 14 2022 at 00:52):

Antoine Labelle said:

For undirected multigraphs, you can always use docs#quiver.has_involutive_reverse, which is relatively close to the definition proposed in #16100 but is already there in mathlib.

Unfortunately, for flow networks, I will need a directed graph.

#### Antoine Labelle (Dec 14 2022 at 03:45):

Aleksandar Milchev said:

Unfortunately, for flow networks, I will need a directed graph.

Well then it's just quivers without the involutive reverse. :smile:

#### Shreyas Srinivas (Dec 15 2022 at 12:37):

Martin Dvořák said:

Aleksandar Milchev said:

Hello! I am a new user and I would like to contribute to the library by implementing a proof for the Max-Flow Min-Cut theorem for flow networks. How should I do that? Is there someone else, who is working on that and if yes, how should I approach the implementation of the proof in that case?
I am also new to lean and all materials that can be helpful (or relevant to the topic) will be much appreciated.

In order to follow any of the classical proofs (you first have to prove that the Max-Flow exists), you will need to implement a Max-Flow algorithm in Lean first. This will require a non-trivial amount of functional programming. Do you have any experience with that?

Do we need an implementation, if we can implement a library for linear programming and prove the strong duality theorem? Speaking of which, from a theoretical CS perspective it seems proofs around linear optimisation might be useful. Is there (mathlib or otherwise) support for this?

(deleted)

#### Shreyas Srinivas (Dec 15 2022 at 13:03):

Shreyas Srinivas said:

Martin Dvořák said:

Aleksandar Milchev said:

Hello! I am a new user and I would like to contribute to the library by implementing a proof for the Max-Flow Min-Cut theorem for flow networks. How should I do that? Is there someone else, who is working on that and if yes, how should I approach the implementation of the proof in that case?
I am also new to lean and all materials that can be helpful (or relevant to the topic) will be much appreciated.

In order to follow any of the classical proofs (you first have to prove that the Max-Flow exists), you will need to implement a Max-Flow algorithm in Lean first. This will require a non-trivial amount of functional programming. Do you have any experience with that?

Do we need an implementation, if we can implement a library for linear programming and prove the strong duality theorem? Speaking of which, from a theoretical CS perspective it seems proofs around linear optimisation might be useful. Is there (mathlib or otherwise) support for this?

Even the typical residual graph based proof does not require an implementation as far as I can tell.

#### Martin Dvořák (Dec 16 2022 at 08:45):

Shreyas Srinivas said:

Do we need an implementation, if we can implement a library for linear programming and prove the strong duality theorem? Speaking of which, from a theoretical CS perspective it seems proofs around linear optimisation might be useful. Is there (mathlib or otherwise) support for this?

As far as I understand the Strong Duality Theorem, we need to show that Max-Flow exists, and then it provides equality to Min-Cut. Alternatively, we can first show that Min-Cut exists, and then it provides equality to Max-Flow.

#### Martin Dvořák (Dec 16 2022 at 08:48):

The latter will be easier, I think. The existence of Min-Cut should be easy to prove without implementation of the search.

#### Martin Dvořák (Dec 16 2022 at 08:51):

Is it easy to prove Farkas lemma from this theorem?
https://github.com/leanprover-community/mathlib/blob/bd59f822dd31da0b6eb683edd04ec01311210066/src/analysis/convex/cone/basic.lean#L847

#### Yaël Dillies (Dec 16 2022 at 08:53):

I think someone has the Farkas lemma somewhere?

#### Martin Dvořák (Dec 16 2022 at 08:54):

Second question: Do we have API for gluing two matrices together?

#### Yaël Dillies (Dec 16 2022 at 08:56):

It's already done in, for example, file#linear_algebra/matrix/block

#### Martin Dvořák (Dec 16 2022 at 09:53):

Yaël Dillies said:

I think someone has the Farkas lemma somewhere?

In case someone has a link, please, send it; I am really interested!

#### Apurva Nakade (Dec 16 2022 at 10:06):

Hi there, here's Farkas lemma in mathlib: docs#convex_cone.hyperplane_separation_of_nonempty_of_is_closed_of_nmem

#### Eric Wieser (Dec 16 2022 at 10:07):

Note that docs#Farkas finds it too

#### Apurva Nakade (Dec 16 2022 at 10:07):

I haven't been able to work on LP versions of this for lack of time :(, so that one is still missing

#### Martin Dvořák (Dec 16 2022 at 10:18):

Hi there, here's Farkas lemma in mathlib: docs#convex_cone.hyperplane_separation_of_nonempty_of_is_closed_of_nmem

That's literally what I was referencing in my question above.

#### Martin Dvořák (Dec 16 2022 at 10:18):

Martin Dvořák said:

Is it easy to prove Farkas lemma from this theorem?
https://github.com/leanprover-community/mathlib/blob/bd59f822dd31da0b6eb683edd04ec01311210066/src/analysis/convex/cone/basic.lean#L847

..

#### Kevin Buzzard (Dec 16 2022 at 10:21):

Well then the question seems to have become "what do you think Farkas' lemma says?".

#### Eric Wieser (Dec 16 2022 at 10:22):

It looks like convex_cone.hyperplane_separation_of_nonempty_of_is_closed_of_nmem only states half of what wikipedia says is the geometric interpretation

#### Eric Wieser (Dec 16 2022 at 10:24):

Oh, actually I guess the other half is trivial, it's just b \in K, and follows from docs#or_iff_not_imp_left; maybe "exactly one" isn't capured accurately

#### Martin Dvořák (Dec 16 2022 at 10:25):

Kevin Buzzard said:

Well then the question seems to have become "what do you think Farkas' lemma says?".

I use these three versions:
image.png

(deleted)

(deleted)

(deleted)

#### Martin Dvořák (Dec 16 2022 at 10:27):

Let me think which of them will yield the most useful version of the Strong Duality Theorem for the sake of proving MaxFlow = MinCut.

#### Martin Dvořák (Dec 16 2022 at 10:40):

I think the last one will be best.

#### Shreyas Srinivas (Dec 16 2022 at 10:56):

Martin Dvořák said:

Kevin Buzzard said:

Well then the question seems to have become "what do you think Farkas' lemma says?".

I use these three versions:
image.png

I suspect that from a CS perspective, we might want a proof from scratch anyway, considering how Farkas Lemma is taught in the typical optimization course.

#### Shreyas Srinivas (Dec 16 2022 at 11:01):

At least the very least, if I claim in some presentation in my department, that I am proving Farkas lemma via the Hahn-Banach separation theorem, then it is a fair guess that the immediate reaction would be "can you provide a simpler proof using elementary ideas?"

#### Martin Dvořák (Dec 16 2022 at 11:03):

Shreyas Srinivas said:

I suspect that from a CS perspective, we might want a proof from scratch anyway, considering how Farkas Lemma is taught in the typical optimization course.

I guess you want to prove one of the three matrix-formulation Farkas Lemmas from scratch (without using geometry). The other two will be reduced to the first Farkas Lemma.

#### Martin Dvořák (Dec 16 2022 at 11:07):

That said, I don't think that the Lean/mathlib community is keen on creating proofs using the most elementary tools only.

#### Shreyas Srinivas (Dec 16 2022 at 11:07):

Martin Dvořák said:

Shreyas Srinivas said:

I suspect that from a CS perspective, we might want a proof from scratch anyway, considering how Farkas Lemma is taught in the typical optimization course.

I guess you want to prove one of the three matrix-formulation Farkas Lemmas from scratch (without using geometry). The other two will be reduced to the first Farkas Lemma.

Yes. something like that. I have not found the relevant set up for linear programming and integer programming yet in mathlib. Even if there is some higher level abstraction in there, we need something at the right level of abstraction

#### Shreyas Srinivas (Dec 16 2022 at 11:08):

Martin Dvořák said:

Shreyas Srinivas said:

I suspect that from a CS perspective, we might want a proof from scratch anyway, considering how Farkas Lemma is taught in the typical optimization course.

I guess you want to prove one of the three matrix-formulation Farkas Lemmas from scratch (without using geometry). The other two will be reduced to the first Farkas Lemma.

Perhaps we need a tcslib

#### Martin Dvořák (Dec 16 2022 at 11:09):

Might be partially relevant: https://leanprover.zulipchat.com/#narrow/stream/236449-Program-verification/topic/Linear.20programming

#### Yaël Dillies (Dec 16 2022 at 11:55):

There's an interesting implementation of linear programming in Coq iirc.

#### Leo Ericson (Dec 16 2022 at 12:04):

Aleksandar Milchev said:

Hello! I am a new user and I would like to contribute to the library by implementing a proof for the Max-Flow Min-Cut theorem for flow networks. How should I do that? Is there someone else, who is working on that and if yes, how should I approach the implementation of the proof in that case?
I am also new to lean and all materials that can be helpful (or relevant to the topic) will be much appreciated.

Hello!

Me and a friend were working on a proof of the Max-Flow Min-Cut theorem this summer! We didn't manage to finish it though, so there's a fair bit left. Here's the repo: https://github.com/Zetagon/maxflow-mincut

One thing to keep in mind is that we weren't planning to contribute to mathlib as our first priority, so there's some stuff that you'd have to change. I think copied and modified Mathlib's quiver for example.

We have a Latex document on overleaf too, I'll commit it to the repository shortly.

#### Leo Ericson (Dec 17 2022 at 10:59):

I apparently forgot to push the report :sweat_smile: It's up now. The style file has some lines commented out because I couldn't get document to compile, uncomment them at your own peril. @Aleksandar Milchev

#### Martin Dvořák (Dec 17 2022 at 11:38):

Can you upload the pdf as well?

#### Leo Ericson (Dec 17 2022 at 12:13):

Done. I commited the pdf directly which feels a bit weird since it's an artifact, but I guess it works.

#### Aleksandar Milchev (Dec 17 2022 at 13:00):

Leo Ericson said:

I apparently forgot to push the report :sweat_smile: It's up now. The style file has some lines commented out because I couldn't get document to compile, uncomment them at your own peril. Aleksandar Milchev

Thank you very much! I will have a look in the following week and may contact you directly after the Christmas break if I have any questions!

#### Leo Ericson (Dec 17 2022 at 13:38):

Yeah go ahead! We'll see how much I remember though...

#### Jihoon Hyun (Dec 27 2022 at 16:55):

Hello, I'd like to use mathlib for discrete maths, and thus want to contribute what is required before and after finset. In order to do so I need some permissions to the github repo.

#### Kevin Buzzard (Dec 27 2022 at 17:02):

Are you talking about lean 3 or lean 4, and what's your GitHub username?

#### Jihoon Hyun (Dec 27 2022 at 17:04):

I'm talking about lean 4, and my github username is qawbecrdtey.

#### Kevin Buzzard (Dec 27 2022 at 17:59):

@maintainers do you also do mathlib4 requests?

yes

#### Aleksandar Milchev (Jan 09 2023 at 10:22):

Hello! As a new member, I want to contribute to mathlib by implementing Bezout's identity and Euler's totient theorem. For the second I will be happy to get some advice on defining Euler's function (specifically the way to count the coprime numbers before n) and defining the reduced residue system modulo n. Thank you!

#### Yaël Dillies (Jan 09 2023 at 10:24):

Hey! We already have docs#zmod, docs#nat.totient and docs#zmod.pow_totient :wink:

#### Yaël Dillies (Jan 09 2023 at 10:25):

Bézout's identity is docs#exists_gcd_eq_mul_add_mul

#### Aleksandar Milchev (Jan 09 2023 at 15:53):

Yaël Dillies said:

Hey! We already have docs#zmod, docs#nat.totient and docs#zmod.pow_totient :wink:

Hey! Thank you for the references! Do you have the general formula of Euler's totient function (the one using the prime factors of n)?

#### Riccardo Brasca (Jan 09 2023 at 15:56):

See docs#nat.totient_eq_div_factors_mul and the theorems around it

#### Aleksandar Milchev (Jan 09 2023 at 16:40):

Riccardo Brasca said:

See docs#nat.totient_eq_div_factors_mul and the theorems around it

Thank you for that! I found the formula.

Sorry for the many questions, but I looked carefully at all results about the int.floor function, but couldn't find floor (floor(x)/n) = floor(x/n) and floor (x+1/2) = floor (2x) - floor(x). There is an interesting fact about floor(m/n), which follows from the first result as well. Did I miss something or these are not in mathlib? If they aren't, I will be happy to implement them. Thank you!

#### Johan Commelin (Jan 09 2023 at 17:10):

Let's see... docs#floor_div

#### Johan Commelin (Jan 09 2023 at 17:11):

The first hit seems to be the first formula you mentioned.

#### Aleksandar Milchev (Jan 09 2023 at 17:21):

Johan Commelin said:

Let's see... docs#floor_div

I tried to follow the link, but it said that the page is no longer available, so I just looked at https://leanprover-community.github.io/mathlib_docs/algebra/order/floor.html#nat.floor_div_nat, but it is not the same as the result I mentioned as it says that floor (a/n) = a/n if we use natural division.

#### Ruben Van de Velde (Jan 09 2023 at 17:33):

You get a 404 error, but below that you get a list of matches

#### Aleksandar Milchev (Jan 09 2023 at 19:47):

Ruben Van de Velde said:

You get a 404 error, but below that you get a list of matches

Yeah, I looked at the matches, but there doesn't seem to be the same.
The one you have sent says that floor(m/n) = m/n using integer division, so it's not the same. The result I want to prove is that for all real numbers x and n, we have floor(floor(x)/n) = floor(x/n), using normal division.

#### Yaël Dillies (Jan 09 2023 at 21:33):

This is what docs#nat.floor_div_nat says.

#### Yaël Dillies (Jan 09 2023 at 21:35):

For any natural number n, floor n = n, so your floor (floor x / n) = floor (x / n) simply becomes floor x / n = x / n, unless you include a coercion to ℚ in the middle, in which case it becomes floor (floor x / n : ℚ) = floor (x / n : ℚ). Then nat.floor_div_nat + nat.floor_div_eq_div gives you the result.

#### Patrick Johnson (Jan 10 2023 at 03:14):

Aleksandar Milchev said:

The result I want to prove is that for all real numbers x and n, we have floor(floor(x)/n) = floor(x/n), using normal division.

That's false. Let $x=n=0.5$, then $\left\lfloor\frac{\left\lfloor{0.5}\right\rfloor}{0.5}\right\rfloor=\left\lfloor\frac0{0.5}\right\rfloor=\left\lfloor0\right\rfloor=0$ and $\left\lfloor\frac{0.5}{0.5}\right\rfloor=\left\lfloor1\right\rfloor=1$

#### Patrick Johnson (Jan 10 2023 at 03:44):

It's true if n is a positive natural number:

import data.real.basic

example {x : ℝ} {n : ℕ} (hn : 0 < n) : ⌊(↑⌊x⌋ : ℝ) / n⌋ = ⌊x / n⌋ :=
begin
apply int.floor_congr, intro k,
have hn' : 0 < (n : ℝ) := by rwa nat.cast_pos,
simp_rw [le_div_iff hn', (by norm_cast : (k : ℝ) * n = ↑(k * n))],
norm_cast, exact int.le_floor,
end


#### Patrick Johnson (Jan 10 2023 at 04:22):

It's also true for n = 0, but only in Lean:

import data.real.basic

example {x : ℝ} {n : ℕ} : ⌊(↑⌊x⌋ : ℝ) / n⌋ = ⌊x / n⌋ :=
begin
cases n, { simp }, apply int.floor_congr, intro k,
have hn' : 0 < (n.succ : ℝ) := by { rw nat.cast_pos, exact ne_zero.pos _ },
simp_rw [le_div_iff hn', (by norm_cast : (k : ℝ) * n.succ = ↑(k * n.succ))],
norm_cast, exact int.le_floor,
end


#### Yaël Dillies (Jan 10 2023 at 06:47):

The lemmas mentioned earlier make it so that you don't need to go down this far in the proof. I am not at a computer right now but you should be able to prove it the way I described in my last message

#### Aleksandar Milchev (Mar 16 2023 at 13:50):

Hey, as mentioned before, I have been working on proving the Max-Flow Min-Cut theorem and have made decent progress so far. Can I please get permission for a PR to the mathlib. My GitHub username is amilchew. Thank you!

Invitation sent!

#### Aleksandar Milchev (Mar 16 2023 at 14:43):

Riccardo Brasca said:

Invitation sent!

Thank you very much! I uploaded a branch max_flow_min_cut and I will do the PR later as my work is still in progress. The purpose of the branch is visibility of the code to my supervisor. Please tell me if I need to do something else. Thank you in advance!

#### Leo Ericson (Mar 16 2023 at 20:40):

Aleksandar Milchev said:

Hey, as mentioned before, I have been working on proving the Max-Flow Min-Cut theorem and have made decent progress so far. Can I please get permission for a PR to the mathlib. My GitHub username is amilchew. Thank you!

Hey, it looks like you've put only your own name in the author and copyright notice. Could you put Leo Okawa Ericson and Viggo Laakshoharju in there as well since it's based on our work?

#### Aleksandar Milchev (Mar 20 2023 at 18:35):

Leo Ericson said:

Aleksandar Milchev said:

Hey, as mentioned before, I have been working on proving the Max-Flow Min-Cut theorem and have made decent progress so far. Can I please get permission for a PR to the mathlib. My GitHub username is amilchew. Thank you!

Hey, it looks like you've put only your own name in the author and copyright notice. Could you put Leo Okawa Ericson and Viggo Laakshoharju in there as well since it's based on our work?

Hey Leo,
I have added your work to the references, but I will happily add you to the authors now as well.
Once again, I appreciate sharing your work, I am doing my best to implement the whole theorem.

#### Leo Ericson (Mar 21 2023 at 10:21):

@Aleksandar Milchev Cool! I hope I didn't come across as too aggressive. They say that imitation is the sincerest form of flattery, but it's almost better when someone is willing to continue upon your work.

(deleted)

#### Patrick Kinnear (Mar 22 2023 at 13:00):

Hi! I've been around Zulip a few months while learning Lean, and I'd like to try contributing to mathlib starting with the baby step of adding some documentation. Could I have github access please? My username is PatrickKinnear

#### Eric Wieser (Mar 22 2023 at 13:06):

Invite sent!

Last updated: Dec 20 2023 at 11:08 UTC