Jiang Jiedong

Stream: new members

[Jiang Jiedong]

Hi everyone,
I am new to Lean and just finished the tutorial project in Lean 3. I feel very excited about idea of formalizing mathematics and want to make some my own contribution to mathlib. I am a phd student in Peking University studying arithmetic geometry, especially p-adic Hodge theory. And I think that through liquid tensor experiment, many definitions and theorems in this field have already been formalized in Lean.
So here are some my questions about what I can do and what I need to do:

1. Before I really contribute to mathlib, what else preparations should I do? Maybe I should get used to lean4 instead of lean3 by writing something? Or should I first read some code already exists? Is there any exercise projects in Lean4?
2. In order to make contribution to mathlib, who should I contact or is there some general guideline? Is there some team I can join?
3. Which part of mathematics can I formalize in mathlib? I don't know how much p-adic Hodge theory has already been formalized and what is left. And as I haven't find the result of liquid tensor experiment appears in the mathlib overview (maybe I missed something?), I wonder if more preparations (probably in commutative algebra and algebraic geometry) should be made before more modern mathematics can be finally convert into mathlib in an systematic and well-organized way? So if I want to make contributions, should I do commutative algebra and algebraic geometry first or can I directly dive into some more advanced p-adic Hodge theory?
   Thanks for any help! Wanna to see more goal accomplished :tada: in Lean :)

[Kevin Buzzard]

Hi! You have arrived at a slightly funny time -- a few months ago the answer would be "use lean 3", in a few months' time the answer will be "use lean 4", and right now the answer is "it's all a bit confusing". Added to this is the issue that our construction of B_{HT} is not yet in mathlib3, even though people are working on B_{dR} and B_{cris}. My instinct is that after that we should be able to start working on the proof that these rings are admissible, so e.g. we can prove $\dim_K(D(V)) <= \dim_{\mathbb{Q}_p}(V)$ for various of the Fontaine functors. If you wanted a nice project which is probably accessible you could try defining admissibility (I learnt about this concept from periodes p-adiques but perhaps there are newer references nowadays) and showing the inequality -- probably best to start in Lean 3. Getting the definition right will be the first step, I can't even remember what it is and my copy of periodes p-adiques is at work :-/

The best way to learn Lean is simply by working on a project. So choose something and go for it :-)

[Johan Commelin]

@Jiang Jiedong Welcome! One clarification: the liquid tensor experiment is in a separate project https://github.com/leanprover-community/lean-liquid that builds on top of mathlib. A lot of the general material has been moving back into mathlib, but there's also lots of general theory that is only in the LTE repo. It has to be cleaned up before it would be ready to go into mathlib.

But then we started porting to mathlib 4, and so in the past 6 months we haven't worked much on contributing new category theory, homological algebra, etc into mathlib. In a couple of months, this should all start moving again.

[Johan Commelin]

As Kevin mentioned above, the period rings are also in a separate project. We do have Witt vectors in mathlib.

[Kevin Buzzard]

@María Inés de Frutos Fernández are you able to formulate precisely in Lean the construction in the theory of Witt vectors which you are missing, in order to get $B_{dR}$ or $B_{dR}(\mathbb{Q}_p)$ from what you have? Can you precisely state the API you need? Or are you working on this yourself and maybe have another idea?

[Kevin Buzzard]

Could this be something @Jiang Jiedong could work on?

[Kevin Buzzard]

The construction of the isomorphism $W(\mathbb{F}_p)\to\mathbb{Z}_p$ is here docs#witt_vector.equiv in mathlib3; that's an example of how to work with Witt vectors.

[Giovanni Mascellani]

Jiang Jiedong said:

1. Before I really contribute to mathlib, what else preparations should I do? Maybe I should get used to lean4 instead of lean3 by writing something? Or should I first read some code already exists? Is there any exercise projects in Lean4?

If I may add something to this, is it difficult to pivot to Lean 4 once you know Lean 3? Would porting stuff from mathlib to mathlib4 be a suggested exercise for newcomers?

[Johan Commelin]

I think the transition should be pretty smooth

[Jiang Jiedong]

Kevin Buzzard said:

Could this be something Jiang Jiedong could work on?

I think its a pretty good start at admissibility and basic properties of period rings such as $ \mathbb{B}_{dr}$ and $\mathbb{B}_{cris}$. I think maybe first write in lean3 then try to convert it in lean4 is good exercise for me.

[Jiang Jiedong]

(deleted)