Diophantine Approximation roadmap

Stream: new members

[Amos Turchet]

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]

Use leanproject

[Jalex Stark]

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

[Jalex Stark]

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

[Jalex Stark]

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

[Jalex Stark]

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

[Jalex Stark]

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

[Jalex Stark]

See #contrib for more details

[Jalex Stark]

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

[Jalex Stark]

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]

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]

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]

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

[Scott Morrison]

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

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]

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]

@Amos Turchet, done!

[Amos Turchet]

Thanks!