# Zulip Chat Archive

## Stream: general

### Topic: Lean job in London

#### Kevin Buzzard (Apr 10 2020 at 17:48):

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 (Apr 10 2020 at 18:00):

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 (Apr 10 2020 at 18:03):

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 (Apr 10 2020 at 18:19):

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

#### Simon Hudon (Apr 10 2020 at 18:37):

How does one apply?

#### Kevin Buzzard (Apr 10 2020 at 18:38):

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 (Apr 10 2020 at 19:48):

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

#### Manuel Eberl (Apr 30 2020 at 14:28):

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

#### Kevin Buzzard (May 03 2020 at 14:37):

It finally got advertised!

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

#### Johan Commelin (May 03 2020 at 14:49):

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

#### Mario Carneiro (May 03 2020 at 15:05):

of plates or call frames or sheaves?

#### Gabriel Ebner (May 03 2020 at 15:07):

Kevin is obviously interested in stack.

#### Patrick Massot (May 03 2020 at 15:07):

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

#### Kevin Buzzard (May 03 2020 at 15:23):

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

#### Kenny Lau (May 03 2020 at 15:24):

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

#### Kevin Buzzard (May 03 2020 at 15:28):

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

#### Kevin Buzzard (May 03 2020 at 15:28):

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

#### Patrick Massot (May 03 2020 at 15:28):

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

#### Kenny Lau (May 03 2020 at 15:34):

yeah you can define stacks in java

#### Kevin Buzzard (May 03 2020 at 15:34):

Maybe we should all switch to Arend

#### Kevin Buzzard (Jan 14 2021 at 23:36):

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.

Last updated: May 14 2021 at 13:24 UTC