Starting a new project

Stream: new members

[Wojtek Wawrów]

Is there some "canonical" tutorial/resource/reference for how one would get around starting a new project of one's own? The tutorials I went through focused solely on proving results given, but didn't discuss how to form new lemmas/theorems/definitions. I could try and extrapolate from looking through the library but I'd rather see a place explaining what does what.
(I am not planning to do it yet, but it would be nice if it also covered defining new types structures)

[Alex J. Best]

For the essentials of making a project directory set up properly you can look at https://leanprover-community.github.io/install/project.html#creating-a-lean-project

[Alex J. Best]

For designing libraries/how to organise developments I think the material from the LFTCM2020 workshop will be helpful, especially Wednesday onwards (e.g. check out the files and exercises on structures, algebra, and topology in https://github.com/leanprover-community/lftcm2020/tree/master/src/exercises_sources/wednesday be sure to clone the whole repo as per the instructions), there are also videos online of some of these sessions, but mostly they were designed for people to learn by doing.

[Alex J. Best]

The main reference as always is #tpil though, if you havent seen it https://leanprover.github.io/theorem_proving_in_lean/structures_and_records.html

[Wojtek Wawrów]

Thanks, I will take a look at all these!

[Antoine Chambert-Loir]

Hi. I plan to spend some time this semester to develop a few things in Lean. I've not done much besides the tutorials. Ultimately, I am interested in formalizing results of graduate level, such as class field theory.
But I might spend a few weeks getting my hands on the system via easier stuff, possibly undergraduate algebra.
@Anne Baanen , @Patrick Massot suggested this morning that we discuss a little bit about it.

[Johan Commelin]

Great to see you again!

[Anne Baanen]

Welcome (back)! I feel somewhat honoured that my name came up, and would be more than happy to assist in getting started with the formalization. Now my background is mostly logic with some algebraic number theory, so I'd like to mention @Filippo A. E. Nuccio whose main area of expertise is CFT. Though I understand Filippo is also busy with the Liquid Tensor Experiment.

So to me the best course of action is probably that I can be here for the first few weeks working on some more elementary topics, and then Filippo is welcome to take over and get into the real meat of CFT.

[Riccardo Brasca]

Needless to say, I am also very interested in CFT... and at only one floor distance from @Antoine Chambert-Loir office :D

[Filippo A. E. Nuccio]

Hi @Antoine Chambert-Loir ! As I was telling @Anne Baanen , @Johan Commelin and @Patrick Massot , I have just submitted a grant proposal to develop some local CFT in Lean, so this is where I will be heading to soon. I would be very much happy to discuss and to take over from @Anne Baanen , although I won't be able to make this my main focus until the end of 2021.

[Anne Baanen]

Perhaps Ostrowski's theorem is a nice place to get started? I think we have most of the ingredients already available in mathlib, so the statement will look something like:

import algebra.order.absolute_value
import analysis.special_functions.pow
import number_theory.padics.padic_norm

noncomputable theory

open real

def absolute_value.trivial : absolute_value ℚ ℝ :=
{ to_fun := λ x, if x = 0 then 0 else 1,
  map_mul' := sorry,
  nonneg' := sorry,
  add_le' := sorry,
  eq_zero' := sorry }

def absolute_value.padic (p : ℕ) [fact (nat.prime p)] : absolute_value ℚ ℝ :=
{ to_fun := λ x, padic_norm p x,
  map_mul' := λ x y, by exact_mod_cast padic_norm.mul p x y,
  nonneg' := sorry,
  add_le' := sorry,
  eq_zero' := sorry }

theorem absolute_value_rat_eq_or_eq (abv : absolute_value ℚ ℝ) :
  (∃ (c : ℝ), (∃ p (hp : nat.prime p), ∀ x, (abv x) ^ c = @absolute_value.padic p ⟨hp⟩ x)) ∨
  (∃ (c : ℝ), ∀ x, (abv x) ^ c = absolute_value.abs x) ∨
  (∀ x, abv x = absolute_value.trivial x) :=
sorry

[Johan Commelin]

@Ryan Lahfa has a formalization of Ostrowski in Lean

[Anne Baanen]

Never mind then :grinning:

[Johan Commelin]

https://github.com/RaitoBezarius/berkovich-spaces

[Adam Topaz]

Hi Antoine! You can count me in as yet another person who is interested in formalizing class field theory. I would like to eventually be able to formalize some aspects of anabelian geometry, where CFT (including the higher dimensional variants) is a fundamental tool.

[Alex J. Best]

Given that #2819 is sorry free and slowly being PRed, and we have finiteness of the class group, maybe some things like Dirichlet's (S-)unit theorem might be in reach now and a good project?

[Adam Topaz]

I think even the basic theory of ramification is currently missing and would be a good project. There is a lot to do!

[Kevin Buzzard]

The next missing definition, in my opinion, is the definition of a local field. There is already a discussion here about whether we just do non-arch char 0, non-arch char 0 and then $\R$ and its finite extensions in three different cases or whether we try and do them all at once. My instinct is to stick to the non-arch case but I don't know whether one should be formalising the theory of complete DVRs which are locally compact wrt the adic topology, or breaking up the theory into a char 0 and a char p strand immediately. I guess I am actually perhaps thinking too hard about the arithmetic case -- the general theory should be developed for arbitrary residue field.

One big missing theorem is the canonical topology on a finite-dimensional vector space over a field like $\mathbb{Q}_p$. In what generality should we have this? Extensions of valuations need doing, as far as I know we don't have that a finite extension of $\mathbb{Q}_p$ has a canonical valuation on it extending the valuation on $\mathbb{Q}_p$ and I haven't really collected my thoughts yet about what order things should be proved in.

[Adam Topaz]

@Kevin Buzzard I think this is a good place to use henselianity :)

[Johan Commelin]

Kevin Buzzard said:

One big missing theorem is the canonical topology on a finite-dimensional vector space over a field like $\mathbb{Q}_p$. In what generality should we have this?

Relevant: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Topology.20of.20finite-dimensional.20real.20vector.20spaces/near/255193392
We almost have this.

[Antoine Chambert-Loir]

@Filippo A. E. Nuccio If you submitted a grand to do this, I feel I shouldn't walk on your steps and leave you this task.
(Anyway, I spend 2 hours today generalizing a small topological lemma in topology.connected, that I'll eventually submit, and in the forthcoming weeks, I'll do little job like this to get more and more fluent in this business.)

[Antoine Chambert-Loir]

Alex J. Best said:

Given that #2819 is sorry free and slowly being PRed, and we have finiteness of the class group, maybe some things like Dirichlet's (S-)unit theorem might be in reach now and a good project?

In fact, doing basic (global) algebraic number theory seems like an interesting, useful and necessary thing to do. In the spirit of the classic books (Borevich-Shafarevich or Samuel).

[Antoine Chambert-Loir]

Kevin Buzzard said:

The next missing definition, in my opinion, is the definition of a local field. There is already a discussion here about whether we just do non-arch char 0, non-arch char 0 and then $\R$ and its finite extensions in three different cases or whether we try and do them all at once. My instinct is to stick to the non-arch case but I don't know whether one should be formalising the theory of complete DVRs which are locally compact wrt the adic topology, or breaking up the theory into a char 0 and a char p strand immediately. I guess I am actually perhaps thinking too hard about the arithmetic case -- the general theory should be developed for arbitrary residue field.

One big missing theorem is the canonical topology on a finite-dimensional vector space over a field like $\mathbb{Q}_p$. In what generality should we have this? Extensions of valuations need doing, as far as I know we don't have that a finite extension of $\mathbb{Q}_p$ has a canonical valuation on it extending the valuation on $\mathbb{Q}_p$ and I haven't really collected my thoughts yet about what order things should be proved in.

In the spirit of the first chapter of Weil's Basic number theory. Yes, why not. This builds on completeness rather than compactness, which is interesting too.

[Filippo A. E. Nuccio]

@Antoine Chambert-Loir My experience with Lean is that contributing is really the key: as I was beginning here, @Anne Baanen was working hard on Dedekind domains, but they suggested that I join forces and it eventually turned out in a joint project (where I did 10% and they did 90%, but I learnt and enjoyed it a lot...). So, I think that there will be a lot of room for common work, if you so wish. I will certainly keep you up to date as soon as I will begin working on local CFT (somewhen in January, when the Liquid Tensor Experiment will be more advanced) and we will see. If, in the meantime, you feel like working either towards the definition of local fields, or Dirichlet's Unit Theorem (global, sure, but possibly more "basic"), or anything else, please do not feel any bound.