Contributing to mathlib

Stream: new members

[Stuart Presnell]

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?

[Bryan Gin-ge Chen]

Invite sent! https://github.com/leanprover-community/mathlib/invitations

[Stuart Presnell]

Great, thank you!

[Scott Morrison]

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

[Stuart Presnell]

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]

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]

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]

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]

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]

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]

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]

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]

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

[Stuart Presnell]

Thanks very much

[Will Sawin]

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]

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]

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

[Kevin Buzzard]

Or Coq

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Stuart Presnell]

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]

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

[Eric Wieser]

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]

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]

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]

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]

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]

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

[Will Sawin]

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]

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

[Patrick Massot]

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]

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]

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]

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]

@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]

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]

Done (with great pleasure!).

[Vincent Beffara]

Thanks!

[Jeoff Lee]

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]

Looks like you have access now, right?

[Johan Commelin]

@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

[Jeoff Lee]

Thanks a lot!

[Ella Yu]

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!

[Bryan Gin-ge Chen]

Invite sent! https://github.com/leanprover-community/mathlib/invitations

[Aleksandar Milchev]

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]

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

[Martin Dvořák]

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]

Are you going to prove it for rational capacities?

[Aleksandar Milchev]

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]

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

[Martin Dvořák]

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

[Yuyang Zhao]

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]

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

[Yaël Dillies]

Currently butchering the rest of my todo list.

[Aleksandar Milchev]

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]

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]

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]

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]

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]

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?

[Shreyas Srinivas]

(deleted)

[Shreyas Srinivas]

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]

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]

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]

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]

I think someone has the Farkas lemma somewhere?

[Martin Dvořák]

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

[Yaël Dillies]

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

[Martin Dvořák]

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!

[Yaël Dillies]

@Apurva Nakade, do you know about this?

[Apurva Nakade]

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

[Eric Wieser]

Note that docs#Farkas finds it too

[Apurva Nakade]

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]

Apurva Nakade said:

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]

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]

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

[Eric Wieser]

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]

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]

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

[Martin Dvořák]

(deleted)

[Martin Dvořák]

(deleted)

[Martin Dvořák]

(deleted)

[Martin Dvořák]

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]

I think the last one will be best.

[Shreyas Srinivas]

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]

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]

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]

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

[Shreyas Srinivas]

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]

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]

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

[Yaël Dillies]

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

[Leo Ericson]

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]

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]

Can you upload the pdf as well?

[Leo Ericson]

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

[Aleksandar Milchev]

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]

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

[Jihoon Hyun]

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]

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

[Jihoon Hyun]

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

[Kevin Buzzard]

@maintainers do you also do mathlib4 requests?

[Mario Carneiro]

yes

[Aleksandar Milchev]

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]

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

[Yaël Dillies]

Bézout's identity is docs#exists_gcd_eq_mul_add_mul

[Aleksandar Milchev]

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]

See docs#nat.totient_eq_div_factors_mul and the theorems around it

[Aleksandar Milchev]

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]

Let's see... docs#floor_div

[Johan Commelin]

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

[Aleksandar Milchev]

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]

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

[Ruben Van de Velde]

Did you need https://leanprover-community.github.io/mathlib_docs/find/nat.floor_div_eq_div ?

[Aleksandar Milchev]

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]

This is what docs#nat.floor_div_nat says.

[Yaël Dillies]

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]

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]

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]

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]

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]

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!

[Riccardo Brasca]

Invitation sent!

[Aleksandar Milchev]

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!

[Eric Wieser]

(branch#max_flow_min_cut)

[Leo Ericson]

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]

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]

@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.

[tica]

(deleted)

[Patrick Kinnear]

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]

Invite sent!