Introductions: Yi Hu

Stream: new members

[Notification Bot]

5 messages were moved here from #Is there code for X? > tensor products commute with direct limits by Johan Commelin.

[Johan Commelin]

@Yi Hu Welcome! I would love to brainstorm with you about what we can do here.

[Johan Commelin]

As far as I can tell, you will need some ingredients in algebraic geometry that we do not have yet: blow-ups and Grassmanians. But with a bit of community effort, I think these are well within reach.

[Johan Commelin]

I have never looked an Mnëv's universality result before. No idea how hard it is to prove that. But it would make sense to treat it as a black box, I think.

[Johan Commelin]

As Heather asked: Do you translate to commutative algebra at some point? Is there a key technical theorem that can be extracted which uses mostly elementary machinery?

[Kevin Buzzard]

Hi @Yi Hu ! I had some email exchange with Lafforgue about this idea -- did he forward it to you? I may as well summarize here anyway. As Heather said we are decent in commutative algebra but right now are weak in the more global aspects of algebraic geometry (we only just got fiber products of schemes for example, and still don't have projective or proper schemes, although people are working on them). These things will happen in time, but it's difficult to know how long they'll take because we rely on teams of volunteers who need to know both the mathematics and how to write the code.

The way big formalisation projects seem to work (these observations are based on empirical experience here) are that to make a project happen you need

*) either a document containing all details of the proof including ones that mathematicians don't normally write down, or constant access to someone (eg you) who knows all these details and who is available to help out;

*) One or more "formalisation leaders" who take on the task of breaking down the project into reasonable steps, setting milestones etc and driving the project followers (this can take up a lot of time, it might end up being the only research project they work on, and of course this can take implications on someone's career path)

*) A team of people who are prepared to help out because they believe in the project.

With the resolution paper my personal opinion is that it's a bit too early to get started, because the human community has not really had time to start making an informed decision about whether the proof is ok. With the Scholze project this also wasn't the case in some sense but it was a much smaller manuscript and the technical point which nobody had checked could be isolated and was only a few pages and in some sense elementary. The other thing i worry about is finding a formalisation leader for the project. Right now because this area is so new it might be difficult to find an appropriate person, especially because the human community haven't really had time to react to the preprint. Can you give some kind of estimate as to how much of the paper is "essentially comprehensible to an MSc student once they have understood the notation"?

[Johan Commelin]

I really think it matters a lot whether you can extract some technical claims about polynomials. Or whether we really need a huge API for AG.

[Yi Hu]

The key portion of proofs only rely on: product of schemes, polynomial equations in affine charts.

[Johan Commelin]

That's certainly something that mathlib/lean can handle right now.

[Yi Hu]

Hi Johan,

We can put Mnev's universality aside, that portion (Section 10) can be verified by human reviewer straightforwardly. The key sections are Sections 4 - 9.

We finesse Grassmanianns and blowups. Instead, we can replace a Grassmannian by the Plucker projective space together with Plucker equations (or just affine charts of the above). Instead of using general blowup (which requires Proj), we can use the most simple ones: (locally) blowing up an affine space V along a co-dimension two coordinate subspace (x=y=0). This can be realized as V \times P^1 and a single equation xv-yu=0. For closed subscheme X of V (that is not contained in the center (x=y=0)) with a family of polynomial equations, the induced blowup on X can be described by proper transforms of the above family of polynomial equations.

The above form the core of the proofs of my paper. It is (complicated, a lot of notations) but very elementary in essence.

[Johan Commelin]

Thanks. How hard would it be to write down the key technical statement in these elementary terms?

[Johan Commelin]

I mean, a statement (or series of statements) that can be shown to imply the main result, by human verification.

[Yi Hu]

Hi Kevin,

Thanks. Yes, Laurent Lafforgue forwarded your messages to me. He is the main force that drove me to Lean.

To answer some of your questions:

*) I can be available to answer all questions about my paper.

*) It is possible to break down the project into several steps. For example, Grassmannian=Projective space with Plucker equations; Simple blowups of X= X \times P^1 with xv-yu=0; Restricted blowups = proper transforms of polynomial equations; and one more thing which we can discuss later.

*) I would say all materials in Sections 4-9 can be understood by a Msc student if he ignores all the buzzwords and pays his attention only to affine spaces and polynomial equations.

[Yi Hu]

Hi Johan, The final main result is proved in Section 10. But, I believe the experts are more eager to understand sections 4-9 about thin Schubert cells. The main result of Section 9 follows from a full rank statement about Jacobian matrix which in turn depends on a family of polynomial equations.

[Yi Hu]

As mentioned in the messages to Kevin, at the moment, I would think the following steps are necessary.

1. Grassmannian=Projective space with Plucker equations;

2. Simple blowups of a smooth scheme X covered by affine space charts = X \times P^1 with xv-yu=0;

3. Restricted blowups on a closed subscheme of X with a fixed set of polynomial equations = proper transforms of
   these polynomial equations;

4. And, one more step which we can discuss later.

[Johan Commelin]

@Yi Hu Is there a recording of a talk on this paper? That might be an efficient way to get an overview of the strategy.

[Riccardo Brasca]

Something I don't understand is if people are more or less sure the result is correct (this was the case for the LTE, the most skeptical was I think Peter). If there are real mathematical doubts I think formalization will be extremely difficult (but I may be wrong).

[Adam Topaz]

Kevin Buzzard said:

*) One or more "formalisation leaders" who take on the task of breaking down the project into reasonable steps, setting milestones etc and driving the project followers (this can take up a lot of time, it might end up being the only research project they work on, and of course this can take implications on someone's career path)

*) A team of people who are prepared to help out because they believe in the project.

In my opinion these two points will be the most challenging in terms of getting this project up and running (the same can be said for any formalization effort for that matter). Unfortunately, there is currently little academic incentive to invest the massive amounts of time and effort required for such projects.

[Yi Hu]

Hi Johan,

For my talk slides, you can download it here https://sites.google.com/a/math.arizona.edu/yi-hu/publications
(look for Resolution of Singularities -main talk.pdf)

I gave several talks, but I can only find recording video in Caucher Birkar's seminar https://cloud.tsinghua.edu.cn/f/c2a20a7d231e40fb81b9/?dl=1
(The title of this talk is "local resolution" because I focused on thin Schubert cells only, at that time.)

[Yi Hu]

Resolution of thin Schubert cells is the key (and appears to be complicated to the reader. But, totally elementary to me). (The remainder part, \S 10, follows.)

[Jz Pan]

Hi all,

I think maybe we can first try to formalize some technical results which only use elementary polynomial operations.
I was trying formalize Lemma 4.6, I think it's feasible, but... it need to take some time (I was only working for it for several hours).

[Yi Hu]

@Johan Commelin @Riccardo Brasca
Hi All,

Ravi Vakil (Stanford University) just kindly emailed and informed me of that he has posted my talk video at his AG seminar on Feb 25 on youtube.com

https://www.youtube.com/watch?v=wkmDnwx3uRI

Please take a look when you get time. Thanks!

This talk (Feb 25, 2022) was an update of my talk in Caucher Birkar's seminar (Nov. 25, 2021).

Thanks!

--Yi

[Johan Commelin]

@Yi Hu Thanks for the link to that video. Concerning formalizing this proof: I think you should expect to formalize most of this yourself. The community can certainly help you get Lean up and running.
A good starting point for learning Lean is https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/
If you want to install Lean on your own machine, see https://leanprover-community.github.io/get_started.html#regular-install