Zulip Chat Archive

Stream: new members

Topic: What should I do before I start working on something?

Shi Zhengyu (Dec 03 2021 at 13:26):

Hi all,
We are a group of undergraduate students in a research project. We would like to try to formalize Cauchy's Interlacing Theorem into lean code. Is there any recommended step to take before actually doing that? (like issue PR etc.? idk)
Thanks!

Huỳnh Trần Khanh (Dec 03 2021 at 14:20):

oops I don't understand your question

Huỳnh Trần Khanh (Dec 03 2021 at 14:21):

"into lean code" what do you mean by this?

Johan Commelin (Dec 03 2021 at 14:21):

@Huỳnh Trần Khanh I'm confused by your confusion

Johan Commelin (Dec 03 2021 at 14:21):

@Shi Zhengyu Welcome! What experience do you have with Lean?

Johan Commelin (Dec 03 2021 at 14:23):

Do you have a detailed proof that you would like to follow? I think most of the basic prerequisites are available in mathlib. So this seems like a suitable project to get started on.

Shi Zhengyu (Dec 03 2021 at 14:23):

Johan Commelin said:

Shi Zhengyu Welcome! What experience do you have with Lean?

We have finished natural number game as well as most of the tutorials on webpage. Currently we are reading Theorem Proving in Lean and Types and Programming Languages, while trying to experiment with mathilb.

Shi Zhengyu (Dec 03 2021 at 14:24):

Johan Commelin said:

Do you have a detailed proof that you would like to follow? I think most of the basic prerequisites are available in mathlib. So this seems like a suitable project to get started on.

Yes, we have a specific proof to follow :D
https://www.tandfonline.com/doi/abs/10.1080/00029890.2004.11920060

Huỳnh Trần Khanh (Dec 03 2021 at 14:25):

oh that sounds great but I'm confused by the "like issue PR etc." part... do you want to contribute to mathlib? or do you want to start a new project?

Huỳnh Trần Khanh (Dec 03 2021 at 14:25):

I mean if you just want to start your own project then I don't think you need any prerequisites aside from a working Lean installation...

Shi Zhengyu (Dec 03 2021 at 14:28):

Sorry for causing misunderstanding :) yes, we would love to contribute to mathlib if condition permits ... I was just wondering if there is any need to share working progress on certain project so to prevent we work on something others have already close to finish ...

Johan Commelin (Dec 03 2021 at 14:28):

Yes, it's good to share your plans beforehand

Johan Commelin (Dec 03 2021 at 14:28):

I'm not aware of anyone working on this.

Shi Zhengyu (Dec 03 2021 at 14:31):

Thanks!!

Last updated: Dec 20 2023 at 11:08 UTC