41 citations · 109 across the 11 of their papers we have counts for
11 papers
Schemes in Lean
Kevin Buzzard, Chris Hughes, Kenny Lau +3
We tell the story of how schemes were formalised in three different ways in the Lean theorem prover.
Formalising perfectoid spaces
Kevin Buzzard, Johan Commelin, Patrick Massot
Perfectoid spaces are sophisticated objects in arithmetic geometry introduced by Peter Scholze in 2012. We formalised enough definitions and theorems in topology, algebra and geome…
A computation of modular forms of weight one and small level
Kevin Buzzard, Alan Lauder
We report on a computation of holomorphic cuspidal modular forms of weight one and small level (currently level at most ) and classification of them according to the projecti…
Slopes of modular forms
Kevin Buzzard, Toby Gee
We survey the progress (or lack thereof!) that has been made on some questions about the p-adic slopes of modular forms that were raised by the first author in [Buz05], discuss str…
Computing weight one modular forms over $\C$ and $\Fpbar$
Kevin Buzzard
We report on a systematic computation of weight one cuspidal eigenforms for the group in characteristic zero and in characteristic . Perhaps the most surprising resul…
Explicit reduction modulo p of certain 2-dimensional crystalline representations, II
Kevin Buzzard, Toby Gee
We complete the calculations begun in [BG09], using the p-adic local Langlands correspondence for GL2(Q_p) to give a complete description of the reduction modulo p of the 2-dimensi…