2020 Summer Projects

Stream: Xena Summer Projects

[Kevin Buzzard]

I am running summer projects from 30th June to the end of August. I will give two talks per week on Discord and generally will help beginners. The idea is that a student should, at the end of it, have a github repository containing working Lean code, and a little write-up explaining what they have done.

Far more details are here. Things will only get going at the end of June, but I'm setting this up now because people are asking what to do next.

[Anton Lorenzen]

I would be interested! Is this open to not-anymore-but-been-very-recently undergrads too? How open are you to projects that are more on the logic/computation side of maths and have very little overlap with algebra? And would it be possible to start only at the third week or so? German exams are always a bit later than those in the English-speaking world..

[Kevin Buzzard]

I can't offer much supervision on the logic/computation side of things, but you're welcome to join in.

[Jalex Stark]

There are people around here that know things about computation :)

[Kevin Buzzard]

Right :-) This whole thing is just a myth, I'm not going to supervise anything, I'm just going to bring a bunch of people together and get them to ask questions on the chat :-)

[Kevin Buzzard]

Actually I am hoping that my performance will be better than in 2018, when I knew very little about Lean and the students realised very early on that they were better off asking Chris Hughes :rolling_on_the_floor_laughing:

[Kevin Buzzard]

This time I feel much better equipped to deal with basic questions

[Yury G. Kudryashov]

If some of the students will want to fill in some gaps in our analysis library, then I'm ready to help mentoring them.

[Kevin Buzzard]

I think that in June when I am out of marking hell I will try and do the analogue of what Patrick/Ryan/Rocky are doing -- go through Imperial's undergraduate course and figure out what is missing. I have not been paying attention to analysis development in mathlib, although I have been keeping more of an eye on algebra/number theory.

[Jalex Stark]

do you have students? are they mostly interacting on discord?

[Kevin Buzzard]

Yes and yes

[Yury G. Kudryashov]

Could you please tell here what are the projects?

[Kevin Buzzard]

People are doing Dedekind domains, working on why 144 is the largest square in the Fibonacci sequence, doing basic number theory (several groups -- stuff we have already, or probably don't want, in mathlib), basic group theory that we have in mathlib already etc

[Kevin Buzzard]

They're just learning Lean

[Yury G. Kudryashov]

Thank you for the list.

[aris zhu]

Screenshot 2020-07-29 at 13.12.32.png

[aris zhu]

IMG_1C2EAE6ABE0E-1.jpeg

[aris zhu]

I am trying to formulate the summation expression as shown in the picture, but I am not sure why my code gives me error, can someone help me pls?

[Patrick Massot]

It would be much easier to help you if you could copy-paste code (and LaTeX code) instead of images.

[aris zhu]

In particular, a_n is a sequence. My approach to formulate the series is to first express the sum as a function mapping from an int n to the result of summation, then let series be a sequence of sum

[Patrick Massot]

(we'll help you anyway, hold on)

[aris zhu]

Ok one sec pls

[aris zhu]

(sum : λ n : ℕ, ∑ i in range n, (rpow (u n) n))

[aris zhu]

Erm sorry I don’t have the source code for the summation expression

[aris zhu]

Let me try to get the source code out

[Patrick Massot]

import topology.algebra.infinite_sum

open finset
open_locale big_operators

variables (a : ℕ → ℝ)
#check λ N, ∑ n in (range N), (a n)^n

#check has_sum (λ n, (a n)^n)

[aris zhu]

$\sum_{n=1}^{\infty} a_n^n$

[Patrick Massot]

Use $$ to enclose LaTeX code

[aris zhu]

Thanks so much

[aris zhu]

The provided code had no problem, but when I put the sum as one hypothesis, ie
(sum : λ N, ∑ n in (range N), (a n)^n), it gives error under $\lambda$ saying that type expected at λ N, ∑ n in (range N), (a n)^n term has type ℕ → ℝ. why is it so?

[Patrick Massot]

What you write has no meaning and, without further context, it's hard to guess what you imagine the meaning would be

[Kevin Buzzard]

@aris zhu please post compiling code with all imports and within triple back ticks like Patrick did

[aris zhu]

Oh I see, having just one summation expression is just a definition, cannot be a hypothesis.

[aris zhu]

import topology.algebra.infinite_sum

open finset
open_locale big_operators

variables (a : ℕ → ℝ)
#check λ N, ∑ n in (range N), (a n)^n

#check has_sum (λ n, (a n)^n)

/-
import analysis.special_functions.pow
import data.real.basic
import algebra.big_operators
-/

notation `|`x`|` := abs x

def seq_limit (u : ℕ → ℝ) (l : ℝ) : Prop :=
∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l| ≤ ε

open_locale big_operators

lemma series_of_root_numbers_converges
(a : ℕ → ℝ) (l : ℝ) (h_seq : seq_limit a l) (hu : ∀ n : ℕ, a n ≥ 0)
(l_pos : l ≥ 0) (l_lt_one: l < 1) :
-- (sum : λ N, ∑ n in (range N), (a n)^n) :
has_sum (λ n, (a n) ^ n) :=
begin
  sorry
end

[aris zhu]

Now the problem is with has_sum

[Patrick Massot]

You should read more careful the result of my #check has_sum

[Patrick Massot]

It is not a Prop but a predicate on real numbers.

[Patrick Massot]

It becomes a Prop if you give a limit candidate.

[aris zhu]

Oh I see, thanks a lot

[aris zhu]

May I know if there is a way to search in the mathlib about any theorem I want to use? Particularly I want to use completeness of $\mathbb{R}$ so that I can prove that a sequence of real numbers which is bounded above has a supremum. Recently I have been randomly looking into the mathlib folders to see if I can happen to find what I need, but it seems like a rather inefficient way.

[Kevin Buzzard]

Usually one talks about the supremum of a set, not a sequence. Due to the total function principle, every set has a sup :-) it's just that the sup might be 37 and not obey the properties of a sup.

[Jalex Stark]

in order to find it just by navigating the the mathlib source by eye, you'll have to guess the right level of generality for the result

[Jalex Stark]

if you search supremum here https://leanprover-community.github.io/mathlib_docs/
the first result is in order.complete_lattice

[aris zhu]

I am sorry I don’t think I get entirely what you are saying, Kevin. I think you are pointing out my misunderstanding that I should talk about the sup of a set instead of a sequence, or rather a mapping from $\mathbb{N}$ to $\mathbb{R}$. So I should focus on the set formed from output of the mapping from natural number, ie the range of the mapping.

Then I don’t know what you mean by total function principle. I searched online, and only found definition on total function. May I know what the principle you are referring to is and so it leads to your conclusion that every set has a sup? And then I can probably understand what you mean by not obeying the properties of sup

[Kevin Buzzard]

There's something in lean called Sup or sup, I forget, but it makes sense for every set of reals. However it only satisfies the axioms of a supremum for nonempty bounded sets. You should locate its definition in data.real.basic or wherever it is and then take a look at the lemmas after it, maybe they'll help. I'm sorry I can't help more, I can't access lean right now

[Yury G. Kudryashov]

See also docs#conditionally_complete_linear_order
real has an instance of this class.

[Yury G. Kudryashov]

(and it is a conditionally_complete_lattice as well)

[Yury G. Kudryashov]

Also it is a docs#complete_space

[Yury G. Kudryashov]

So any docs#cauchy_seq converges

[Patrick Massot]

Aris, did you try to use the overview pages ?

[aris zhu]

Thank you Kevin and Yuri, I will take a look at those.

[aris zhu]

Patrick, i don’t know what are overview pages, what are those?

[Bryan Gin-ge Chen]

https://leanprover-community.github.io/mathlib-overview.html

You can reach this from the menu on the top right of the community website under "Learn -> Library overview".

[aris zhu]

May I know what is the tactics I can use so that I can define a set as the range of a function? Particularly I would like to define a mapping from N to R, ie sequence, and define the range of the mapping as a set of R

[Kevin Buzzard]

This sounds like set.rangein data.set.basic

[Jalex Stark]

the first three results for searching "range" at the #docs are all relevant

[aris zhu]

Thanks for the tips.

Currently I want to prove that a set is non-empty. I want to prove that given (u : ℕ → ℝ), (∃ (x : ℝ), x ∈ range u). To prove this, I have typed use u 1 to provide the possible value of x, but then I am stuck on the expression ⊢ u 1 ∈ range u. I tried to unfold it, getting ⊢ u 1 ∈ {x : ℝ | ∃ (y : ℕ), u y = x}, but still don't know what should be the appropriate tactics to close this goal. What should be the tactics to prove this?

[Jalex Stark]

what does suggest say?

[Jalex Stark]

i think your goal is defeq to \ex y, u y = u 1, so use 1 should work

[Kevin Buzzard]

yeah @aris zhu you're on the right track. The dsimp tactic will try to unfold definitions and change your goal to something which is the same by definition, but hopefully simpler to understand, so you could try that before Jalex' suggestion, but in fact Jalex' suggestion should work straight out of the box. I'm back in London now so could hopefully be more helpful.

[Reid Barton]

There will also be some lemma with a name like set.mem_range that exactly proves things like u 1 ∈ range u.

[aris zhu]

Jalex Stark said:

what does suggest say?

What do you mean by suggest?

[aris zhu]

Thanks for helping me. use 1 works, however, dsimp does not, neither does set.mem_range.

[Bryan Gin-ge Chen]

suggest is the name of a tactic, it works similarly to library_search except it returns more options, see tactic#suggest

[aris zhu]

wow suggest is a really cool feature!

[aris zhu]

btw, via suggest I also managed to use set.mem_range_self 1 to close the goal, and subsequently there are a lot of refine tactics statements being suggested

[aris zhu]

suggest makes me feel like Lean is almost possible to do proofs on its own! :thinking:

[Jalex Stark]

at the risk of excessively repeating myself, this google search takes you to the definition of suggest as the first hit
https://www.google.com/search?q=suggest%20site%3Ahttps%3A%2F%2Fleanprover-community.github.io%2Fmathlib_docs%2F

[Jalex Stark]

aris zhu said:

suggest makes me feel like Lean is almost possible to do proofs on its own! :thinking:

automation does a lot of work in any modern proof library, in fact moreso in the isabelle and coq libraries than in mathlib. for anyone who likes functional programming enough, there are several open issues in the mathlib github repo describing potential tactics that can automate more for us.

[aris zhu]

Currently I have hM : M ≤ x ↔ ∀ (z : ℝ), z ∈ f_range u → z ≤ x. What is the tactics allow me to change it to something like hM : M ≤ x ↔ ∀ (n : ℕ), u n ≤ x? f_range u is just the range of function u.

[aris zhu]

This time suggest just gives me a lot of refine commands, which are rather useless

[Jalex Stark]

If you do have : M ≤ x ↔ ∀ (n : ℕ), u n ≤ x, then tactics which try to figure things out will know what you're trying to figure out

[Jalex Stark]

another thing I would do here is write
#check mem_range or #check set.mem_range and look at the autocomplete suggestions

[aris zhu]

Jalex Stark said:

another thing I would do here is write
#check mem_range or #check set.mem_range and look at the autocomplete suggestions

Regarding the autocomplete suggestions, do you mean the pop-up window? or something in the Lean Infoview pane? Screenshot-2020-08-03-at-15.48.08.png

[Jalex Stark]

yes I meant that popup window

[Jalex Stark]

indeed it looks like rw mem_range is something you want

[Reid Barton]

aris zhu said:

f_range u is just the range of function u.

What does this mean? Is f_range something you defined?

[Jalex Stark]

you'll have to help it see through your f_range, though

[Jalex Stark]

in general, aliases mostly get in the way

[Reid Barton]

anyways, docs#set.forall_range_iff is what you want

[Reid Barton]

also it's not a tactic

[Reid Barton]

tactics are things like rw, intro

[aris zhu]

Reid Barton said:

aris zhu said:

f_range u is just the range of function u.

What does this mean? Is f_range something you defined?

Yes I defined myself, very close to the definition in mathlib, because I realize that the name overlaps with the range used for $\sum$, so to avoid clashes in names, I defined another f_range, with all its related types specifically being related to what I am proving

[Jalex Stark]

well if you want access to the many lemmas we have about ranges of functions, you should use the mathlib range

[Jalex Stark]

in particular, reid points out the the thing you want to prove is already a lemma in the library about mathlib's range

[aris zhu]

Reid Barton said:

anyways, docs#set.forall_range_iff is what you want

yeah I got this from establishing a lemma like jalex suggested, and used rw hM and suggest to figure out exact set.forall_range_iff

[Jalex Stark]

also, the typical way to deal with name collisions is namespaces. set.range is the thing we're talking about here, and finset.range is probably the one you've seen used with sums

[Jalex Stark]

i would typically not open set and instead just say set.range when I need it

[aris zhu]

what do you mean by open set?

[Reid Barton]

https://leanprover.github.io/theorem_proving_in_lean/dependent_type_theory.html#namespaces

[Reid Barton]

If you're not already using open then there is no danger of a name collision between set.range and finset.range.

[aris zhu]

ok thanks so much

[aris zhu]

Say i have a proposition to be proven, but involves the discussion of comparison of two variables, say a and b. Is there a tactic which I can split the goal into three with different conditions, a > b,a < b, a = b, and then prove the proposition respectively?

[Jalex Stark]

i'm not sure why you ask for a tactic

[Jalex Stark]

i think what you want is the theorem that a < b \or a = b \or b < a

[Jalex Stark]

and then you can use the cases tactic on that theorem

[Jalex Stark]

you should be able to find this theorem with library_search

[aris zhu]

because split allows me to split the goal into two, if it can be split, so I thought there is a way to split inequalities as well

[Jalex Stark]

the thing you want to split on is not in the goal

[Dan Stanescu]

Is this what you're asking for:

rcases lt_trichotomy a b with h1|h2|h3,

@aris zhu

[Jalex Stark]

when we split on hypotheses, that's called cases instead of split

[aris zhu]

ah yeah cases that is

[Jalex Stark]

if you just want to split on p \or \not p for some specific p, you can use by_cases p

[aris zhu]

If I were to write by_cases (M > u 1), it gives me error on >, saying that the inequality is not a Prop, I wonder why inequality is not considered Type Prop?

[Reid Barton]

what is the whole error?

[aris zhu]

function expected at
  M > u 1
term has type
  Prop

[Reid Barton]

You've made some other error which is hard to guess without knowing what you've written

[Reid Barton]

maybe a missing ,

[aris zhu]

thanks so much, silly mistake...

[Reid Barton]

Also, if you read the error message, you'll see it's telling you that M > u 1 is a Prop

[Reid Barton]

but it was expecting a function--probably because you had something after (M > u 1) which Lean interpreted as an argument to it.

[Reid Barton]

Error messages are helpful.

[Reid Barton]

but sometimes they take some puzzle solving to interpret--if Lean is confused, obviously it doesn't know why it's confused, so it's your job to guess why that might be

[aris zhu]

Is there a lemma to convert ¬(A ↔ B) to ¬A ↔ B? I found something similar like not_iff but it doesn't seem to work

[Shing Tak Lam]

I'm not sure that's true constructively, so you'd need classical logic to prove that. Is there an error about type class instances?

Putting open_locale classical in your file should allow you to use not_iff. (or if you can show that B is decidable that would work as well)

[aris zhu]

ah I didn't put open_locale classical. What is the difference between open and open_locale? I searched in the mathlib and found open_locale used for declaring notation as local notation, but for me it seems like a redundant explanation since "opening" a namespace is to use the terms in the namespace in the current script. Also, is there a place describing this kind of dependencies, where I need to add open or open_locale so that I can use the lemmas?

[Jalex Stark]

open opens a namespace

[Jalex Stark]

open_locale brings in local notations and local instances

[Jalex Stark]

anything you can do with open you can also do with dot notation

[Jalex Stark]

eg

import data.finset

#check card
#check finset.card
open finset
#check card

[aris zhu]

Can I clarify with this theorem: theorem exists_sup (S : set ℝ) : (∃ x, x ∈ S) → (∃ x, ∀ y ∈ S, y ≤ x) → ∃ x, ∀ y, x ≤ y ↔ ∀ z ∈ S, z ≤ y. I believe that (∃ x, x ∈ S) means non-empty set S, (∃ x, ∀ y ∈ S, y ≤ x) means set S is bounded above by x. And what I am confused about is ∃ x, ∀ y, x ≤ y ↔ ∀ z ∈ S, z ≤ y. At first I thought that x is the supremum, but then after some considerations, I feel that x is rather a lower bound of the set of upper bounds of S. As such the last sentence should add z ≤ x to show that x is also an upper bounds of S to make it a supremum?

[Patrick Massot]

I think you are confused by precedence issues.

[Patrick Massot]

Try adding parentheses while checking that Lean still thinks this is the same definition.

[Kevin Buzzard]

(x is indeed the supremum)

[aris zhu]

Patrick Massot said:

Try adding parentheses while checking that Lean still thinks this is the same definition.

I am sorry but I still cannot figure out why. The reason I got confused about this, is because I want to use this theorem to identify the supremum, i.e. x, and then derive the conclusion ∀ ε > 0, ∃ n₀, u n₀ ≥ x - ε. What I did is to set up the lemma have lemma : ∃ x, ∀ y, x ≤ y ↔ ∀ z ∈ S, z ≤ y, and used the theorem, together with non-emptiness and bounded above, to prove the lemma. Then when I want to use that lemma to prove ∀ ε > 0, ∃ n₀, u n₀ ≥ x - ε, I just cannot figure out a way, and I realize that it lacks some "bounds" to x in ∃ x, ∀ y, x ≤ y ↔ ∀ z ∈ S, z ≤ y. In terms of precedence, I believe it is ∃ x, (∀ y, (x ≤ y ↔ ∀ z ∈ S, z ≤ y)).

[Reid Barton]

This is slightly tricky. Hint: the fact that ↔ is used is important.

[Kevin Buzzard]

You're right about the precedence. If you let y=x then you see in particular that x is an upper bound.

[aris zhu]

Thanks for helping me clarify the statement and tips for understanding why it is an upper bound. This actually helps me to realize that my problem was to prematurely specialize a ∀ lemma, then I cannot properly use contrapose to prove the result.

[aris zhu]

I want to get from n : ℕ, a n ≥ 0 to deduce a n ^ n ≥ 0? suggest doesn't give any useful hint. I think the name is probably related to pos, pow, and I found one that is closest to what I need, (at least I think it is), exact nat.pos_pow_of_pos _ _, but it is not working for me. The error gives

invalid type ascription, term has type
  0 < ?m_1 ^ ?m_2
but is expected to have type
  a n ^ n ≥ 0

I don't understand the error message regarding m_1, m_2, what are those types? So that I can understand what is wrong with the expression and potentially fix it

[Jason KY.]

What is a?

[aris zhu]

a is a function, a : ℕ → ℝ

[Jason KY.]

pow_nonneg should do it

[Jason KY.]

example (n : ℕ) (a : ℕ → ℝ) (ha : ∀ n, 0 ≤ a n) : 0 ≤ a n ^ n :=
begin
  apply pow_nonneg,
  exact ha n,
end

[aris zhu]

thanks, it works!

[aris zhu]

could you just also explain to me what m_2, m_1 are? are they some kind of general types? if so, how would I know if N or R is a "sub-type" of m_2, m_1?

[Jason KY.]

They are placeholders

[Jason KY.]

pow_pos is for showing positive < while you have \le so lean cant find things to put in the placeholders

[aris zhu]

oh i see, so I should use nonneg and nonpos when I see ≥ 0 and ≤ 0

[aris zhu]

Now I am stuck on this problem, from h : ∀ (n : ℕ), a n ^ n ≥ 0 to deduce 0 ≤ ∑ (n : ℕ) in range m, a n ^ n - ∑ (n : ℕ) in range n, a n ^ n, where nm : ℕ. In my mind I think what I need to do is to simplify the summation expression to something like 0 ≤ ∑ (n : ℕ) in (range m - range n), a n ^ n, and then probably I can directly exact h. What can I do with the summation expression to simplify it?

[Jason KY.]

I've done something similar before simplifying sum to finset.Ico before. Take a look at: https://github.com/JasonKYi/M4000x_LEAN_formalisation/blob/master/src/M40002/M40002_C4.lean#L148 and see if it helps

[aris zhu]

or is there any place I can read more about ∑?

[Jason KY.]

Its a local definition def partial_sum_to (a : ℕ → ℝ) (n : ℕ) := finset.sum (finset.range n) a

[Jason KY.]

With notation ∑ a := partial_sum_to a

[aris zhu]

ok I will take a look! Thanks

[aris zhu]

What would be the tactics to split n ≤ m into n < m and n = m? I tried by_cases n < m but they don't seem to work that well because it ignores the original condition

[Jason KY.]

le_iff_eq_or_lt

[aris zhu]

@Jason KY. , regarding (∑ a) m - (∑ a) n = finset.sum (finset.Ico n m) a, why is it Ico instead of Ioc? I thought that it should be [n + 1, m], i.e. (n, m]?

[Jason KY.]

(∑ a) m is the sum of a n from n = 0 to a = m -1 and finset.Ico n m is the set of nats from n to m -1. The maths works out so I'm not sure whats the confusion

[aris zhu]

oh I though that (∑ a) m is the sum of a n to n = m instead of n = m - 1. Thanks for the clarification

[Kevin Buzzard]

It's a sum of m things

[aris zhu]

How can I break an extremely long line into two lines in Lean?

[aris zhu]

Is it the same as what we do for calc environment, i.e. add ... in front of the line?

[Bryan Gin-ge Chen]

You can just break the line and it should be fine. Lean (usually) ignores whitespace (including line breaks).

[aris zhu]

I am sorry that I cannot find it in library API but what is the theorem I can used to prove that if n ≤ N and ¬n = N, then n < N? I tried with something like le_not_eq, but there doesn't seem to have any option related to this

[Jalex Stark]

You should be able to find it with library search

[Jalex Stark]

docs#library_search

[Jalex Stark]

But also tactic#linarith

[aris zhu]

I tried with linarith but it cannot be used in this situation

[Dan Stanescu]

This works and I got it with library_search:

example (n N : ℕ) (h1 : n ≤ N) (h2 : n ≠ N) : n < N := lt_of_le_of_ne h1 h2

[aris zhu]

ok I think my problem was that I didn't put ne in my search, instead I place not_eq. Thanks for the help

[aris zhu]

regarding specialize tactics, what is the way to retain the original hypothesis? I see in the documentation that it "tries to clear the previous one", can I choose not to do it?

[Kevin Buzzard]

you can just let f2 := f x

[aris zhu]

Is there a reason why for nat.mul_div_mul, that is m > 0 → m * n / (m * k) = n / k, have the restriction m > 0? Why is it not m ≠ 0?

[Kevin Buzzard]

they're equivalent of course, because it's a theorem about naturals, but probably there is some standard form, although I very much doubt the standard way to express this is m>0 because > is persona non grata usually.

[Yury G. Kudryashov]

One of the reasons to use 0 < m instead of m ≠ 0 is that 0 < m and m ≤ n immediately imply 0 < n.

[Yury G. Kudryashov]

Unfortunately, we have no "normal form" here; e.g., many theorems about ennreals use < ∞ and many use ≠ ∞.

[aris zhu]

Kevin Buzzard said:

they're equivalent of course, because it's a theorem about naturals, but probably there is some standard form, although I very much doubt the standard way to express this is m>0 because > is persona non grata usually.

What do you mean by "> is persona non grata usually"?

[aris zhu]

Yury G. Kudryashov said:

One of the reasons to use 0 < m instead of m ≠ 0 is that 0 < m and m ≤ n immediately imply 0 < n.

So is it a design choice so that other theorems/lemmas can derive results easier?

[aris zhu]

what is ennreal? I search on the mathlib and cannot figure what category it means..

[Shing Tak Lam]

mathlib prefers < and ≤ over > and ≥, hence you'll see m > 0 written as 0 < m in mathlib.

[Shing Tak Lam]

ennreal is here https://leanprover-community.github.io/mathlib_docs/data/real/ennreal.html

[aris zhu]

Shing Tak Lam said:

ennreal is here https://leanprover-community.github.io/mathlib_docs/data/real/ennreal.html

yes I found the link, but I don't understand what ennreal means, so just curious if it stands for something?

[Kevin Buzzard]

extended (i.e. contains infinity) non-negative reals

[aris zhu]

May I know what's wrong with the following?
I want to say that $l \in [0, 1)$, and after checking through mathlib I believe I should use def Ico (a b : α) := {x | a ≤ x ∧ x < b} in data.set.intervals.basic, so I wrote hl : l ∈ Ico 0 1, but then error message failed to synthesize type class instance for is given. I did import data.set.intervals.basic at the top.

[Dan Stanescu]

Try l ∈ Ico (0:\R) 1.

[aris zhu]

Hi all! I have finally finished proving my question in Lean! My personal goal for this UROP was to finish proving one question by the end of August, and I managed to do it, even one week faster haha. Thanks for everyone in this channel who has helped me along the way. It was a very different experience I had for proving using code instead of pen and paper. You can checkout my git repo at https://github.com/qsmy41/ICL-UROP---LeanProver

@Jason KY. I used two of your lemmas, and in my repo I commented that the two lemmas are from you. I am not sure if this is the right way to do it, and not sure if you mind me using some of your work. Could you give me some suggestions?

[Kevin Buzzard]

Well done @aris zhu , you can join the club of people who I have indoctrinated :D You should make a better README where you explain in maths terms what the theorem is and how you proved it.

[aris zhu]

ok Let me update it!

[Jason KY.]

I dont mind how you would like to credit. The way you've done so far is perfectly fine by me :)

[Ed]

The discord link is invalid. Is there a new one?

[Kevin Buzzard]

Who are you?

[Ed]

A final year CS undergraduate from the university of Bath. I was speaking to a friend who graduated from maths at ICL last year about category theory and theorem provers. He mentioned lean and that you were welcoming of students from outside ICL. He also mentioned that there was a discord, sent me a link to this forum, and said I should join if I was interested.

I looked up a few videos on YouTube and decided I was interested. So, here I am!

[Yaël Dillies]

Did you manage to get in since then?