Lean job in London

Stream: general

[Kevin Buzzard]

So the COVID19 issue has made it complicated to get admin done, and my job ad is still not out :-(

But basically, at some point in the near future, virus willing, I will be advertising for a three year post-doc position, salary £45000 per year, and the ad will look something like this:

---

Job Summary

Applications are invited for a Research Associate position in the Department of Mathematics at Imperial College London. The position is funded by Imperial College’s Excellence Fund for Frontier Research and will involve teaching various aspects of modern research arithmetic geometry to the Lean Theorem Prover.

Duties and Responsibilities

The project will involve working closely with Professor Kevin Buzzard and the number theory group at Imperial College, and will involve formalising some of the ideas in one or more of the following topics: de Jong’s Stacks Project, the theory of etale cohomology, the Langlands Program (and in particular formalisations of the statements of the main theorems and conjectures), class field theory and arithmetic duality, Scholze’s theory of perfectoid spaces, Lurie’s theory of infinity categories, the Clausen/Scholze theory of condensed sets.

Essential Requirements

The essential requirements for this post are as follow:

• A PhD or equivalent level of professional qualifications and/or experience in either algebraic number theory or formal proof verification.
• Knowledge of, or evidence that you can quickly learn about, some of the basic tools of modern algebraic number theory.
• Knowledge of, or evidence that you can quickly learn about, formalising pure mathematics in the Lean Theorem Prover.
• Ability to carry out original research and to produce published research papers.
• Ability to identify, develop and apply new concepts, techniques and methods.
• Ability to organise and prioritise own work with minimal supervision.
• Ability to prioritise own work in response to deadlines.
• Ability to communicate complex information clearly

---

When it's actually in some published form I'll circulate it in the normal way, but I thought I should flag that this is, hopefully, coming soon. Start date 1st October 2020 or perhaps later, if things are still weird.

[Simon Hudon]

That sounds like a cool job :) As it happen, my CMU contract will be over by then. Any chance you'd consider a computer scientist for the job?

[Kevin Buzzard]

I thought that if I said "need experience in formal proof verification and algebraic number theory" then I would 0 applications, that's why I wrote or :-)

[Simon Hudon]

The union of two (largely) disjoint sets will indeed be much larger :)

[Simon Hudon]

How does one apply?

[Kevin Buzzard]

You have to wait for the ad, which is held up in the system because apparently some people are busy right now with other things

[Vaibhav Karve]

Thanks for the heads-up @Kevin Buzzard. I'll keep my eyes peeled for the formal job ad.

[Manuel Eberl]

Certainly high up in my list of possible postdoc positions to apply to!

[Kevin Buzzard]

It finally got advertised!

https://www.imperial.ac.uk/jobs/description/NAT00701/research-associate-formal-mathematics

[Johan Commelin]

I guess if you want to practice for interview questions... make sure you know what a stack is :wink:

[Mario Carneiro]

of plates or call frames or sheaves?

[Gabriel Ebner]

Kevin is obviously interested in stack.

[Patrick Massot]

You're both out of this competition. Too bad...

[Kevin Buzzard]

https://stacks.math.columbia.edu/tag/026O

[Kenny Lau]

https://docs.oracle.com/javase/7/docs/api/java/util/Stack.html

[Kevin Buzzard]

I think these might be instances of different people using the same word to mean different concepts.

[Kevin Buzzard]

either that or there is some fundamental point which I missed.

[Patrick Massot]

That's probably because you're not familiar with Java

[Kenny Lau]

yeah you can define stacks in java

[Kevin Buzzard]

Maybe we should all switch to Arend

[Kevin Buzzard]

I have money for an 18-month post-doc to formalise research number theory in Lean. Here's the ad:

https://www.imperial.ac.uk/jobs/description/NAT00845/research-associate-formal-mathematics

You'll be working with me, my other post-doc, my PhD student, and a bunch of undergraduates.

The start date has to be before July 31st and there is 18 months of funding. I am not sure that the grant will cover the higher range of the salary being advertised in the advert, but I thought that the sooner I mentioned the ad the better.