Zulip Chat Archive

Stream: new members

Topic: Diophantine Approximation roadmap

Amos Turchet (Aug 02 2020 at 15:20):

Me and a fellow colleague were interested in trying to get our hands dirty with Lean and were thinking to start a project to formalize some basic Diophantine Approximation results with the (longterm) goal to prove Thue's and Roth's Theorems (and possibly their applications to solutions of Diophantine Equations).
Would that be of interested of the community? What is the best way to start other than create the lean file, do the work, and then have it somewhere on Github for people to see it?

Jalex Stark (Aug 02 2020 at 15:35):

Use leanproject

Jalex Stark (Aug 02 2020 at 15:36):

This makes it easy for other people to run your project without worrying about what version of mathlib it depends on

Jalex Stark (Aug 02 2020 at 15:36):

The theorems you suggest are theorems that should end up in mathlib

Jalex Stark (Aug 02 2020 at 15:37):

As soon as you have a chunk of your project which can be PRed to mathlib, you should do it

Jalex Stark (Aug 02 2020 at 15:38):

This will get some code review and may change how you approach the rest of the project

Jalex Stark (Aug 02 2020 at 15:38):

In fact for a project like this, many people prefer to develop on a branch in the mathlib repo

Jalex Stark (Aug 02 2020 at 15:39):

See #contrib for more details

Jalex Stark (Aug 02 2020 at 15:39):

More importantly, come back and ask questions whenever you get stuck

Jalex Stark (Aug 02 2020 at 15:41):

In addition to helping you finish your project more quickly, the community is producing intro materials, most notably #mil. This development is guided in part by questions from mathematicians on zulip

Alex J. Best (Aug 02 2020 at 17:03):

Diophantine approximation sounds great! You might be interested in checking out some of
@Jujian Zhang's work at https://github.com/jjaassoonn/transcendental which isn't in mathlib but has some nice results (Liouville's theorem for one)

Scott Morrison (Aug 03 2020 at 02:46):

Since this is material we'd love to have in mathlib, it may make sense to just work in a branch of mathlib, rather than a separate repository.

Scott Morrison (Aug 03 2020 at 02:46):

This makes it easy to get material ready for a PR to mathlib, when you reach this stage.

Scott Morrison (Aug 03 2020 at 02:47):

(Getting material through the PR process is extra work, sometimes a lot of extra work, but hopefully your code ends up better, you learn a lot about Lean from the process, and the mathematical development is then available and easily usable by everyone else.)

Scott Morrison (Aug 03 2020 at 02:48):

If you want permission to push to non-master branches of the main repository of mathlib, just ask here. (Alternatively, you can always fork the mathlib repository on github. The main advantages of working in a branch on the main repository are that you get the benefit of olean files built by our continuous integration setup, and during the review process of a PR it's a little easier for reviewers.)

Amos Turchet (Aug 05 2020 at 09:12):

Looks like working on a branch of mathlib makes the most sense then. Is it possible to have permission? My GitHub user name is amosturchet. THANKS!

Scott Morrison (Aug 05 2020 at 09:13):

@Amos Turchet, done!

Amos Turchet (Aug 05 2020 at 09:14):


Last updated: Dec 20 2023 at 11:08 UTC