## Publications

28 results found

Buzzard K, Commelin J, Massot P, 2020, Formalising perfectoid spaces, POPL: Principles of Programming Languages, Publisher: Association for Computing Machinery, Pages: 299-312

Perfectoid spaces are sophisticated objects in arithmetic geometry introducedby Peter Scholze in 2012. We formalised enough definitions and theorems intopology, algebra and geometry to define perfectoid spaces in the Lean theoremprover. This experiment confirms that a proof assistant can handle complexityin that direction, which is rather different from formalising a long proofabout simple objects. It also confirms that mathematicians with no computerscience training can become proficient users of a proof assistant in arelatively short period of time. Finally, we observe that formalising a pieceof mathematics that is a trending topic boosts the visibility of proofassistants amongst pure mathematicians.

Buzzard K, Verberkmoes A, 2018, Stably uniform affinoids are sheafy, *Journal fur die Reine und Angewandte Mathematik*, Vol: 740, Pages: 25-39, ISSN: 0075-4102

We develop some of the foundations of affinoid pre-adic spaces withoutNoetherian or finiteness hypotheses. We give some explicit examples of non-adicaffinoid pre-adic spaces (including a locally perfectoid one). On the positiveside, we also show that if every affinoid subspace of an affinoid pre-adicspace is uniform, then the structure presheaf is a sheaf; note in particularthat we assume no finiteness hypotheses on our rings here. One can use ourresult to give a new proof that the spectrum of a perfectoid algebra is an adicspace.

Buzzard K, Lauder A, 2016, A computation of modular forms of weight one and small level, *Annales mathématiques du Québec*, Vol: 41, Pages: 213-219, ISSN: 2195-4763

We report on a computation of holomorphic cuspidal modular forms of weight one and small level (currently level at most 1500) and classification of them according to the projective image of their attached Artin representations. The data we have gathered, such as Fourier expansions and projective images of Hecke newforms and dimensions of space of forms, is available in both Magma and Sage readable formats on a webpage created in support of this project.

Buzzard K, Gee T, 2016, Slopes of Modular Forms, Simons Symposium on Families of Automorphic Forms and the Trace Formula, Publisher: SPRINGER INTERNATIONAL PUBLISHING AG, Pages: 93-109, ISSN: 2365-9564

Buzzard K, Ciere M, 2014, Playing simple loony dots and boxes endgames optimally, *Integers: electronic journal of combinatorial number theory*, Vol: 14, ISSN: 1553-1732

We explain a highly efficient algorithm for playing the simplest type of dotsand boxes endgame optimally (by which we mean "in such a way so as to maximisethe number of boxes that you take"). The algorithm is sufficiently simple thatit can be learnt and used in over-the-board games by humans. The types ofendgames we solve come up commonly in practice in well-played games on a 5x5board and were in fact developed by the authors in order to improve theirover-the-board play.

Buzzard K, Gee T, 2014, The conjectural connections between automorphic representations and Galois representations, *AUTOMORPHIC FORMS AND GALOIS REPRESENTATIONS, VOL 1*, Vol: 414, Pages: 135-187, ISSN: 0076-0552

- Author Web Link
- Cite
- Citations: 20

Buzzard K, Gee T, 2013, Explicit reduction modulo p of certain 2-dimensional crystalline representations, II, *Bulletin of the London Mathematical Society*, Vol: 45, Pages: 779-788, ISSN: 1469-2120

We complete the calculations begun in Buzzard and Gee (Int. Math. Res. Not. IMRN 12 (2009) 2303–2317), using the p-adic local Langlands correspondence for GL2(ℚp) to give a complete description of the reduction modulo p of the 2-dimensional crystalline representations of Gℚp of slope less than 1, when p > 2.

Buzzard K, 2011, Computing weight one modular forms over $\C$ and $\Fpbar$, Computations with Modular Forms 2011

We report on a systematic computation of weight one cuspidal eigenforms forthe group $\Gamma_1(N)$ in characteristic zero and in characteristic $p>2$.Perhaps the most surprising result was the existence of a mod 199 weight~1 cuspform of level 82 which does not lift to characteristic zero.

Buzzard K, Diamond F, Jarvis F, 2010, ON SERRE'S CONJECTURE FOR MOD l GALOIS REPRESENTATIONS OVER TOTALLY REAL FIELDS, *DUKE MATHEMATICAL JOURNAL*, Vol: 155, Pages: 105-161, ISSN: 0012-7094

- Author Web Link
- Open Access Link
- Cite
- Citations: 70

Buzzard K, Gee T, 2009, Explicit Reduction Modulo p of Certain Two-Dimensional Crystalline Representations, *INTERNATIONAL MATHEMATICS RESEARCH NOTICES*, Vol: 2009, Pages: 2303-2317, ISSN: 1073-7928

- Author Web Link
- Open Access Link
- Cite
- Citations: 21

Buzzard KM, 2007, Eigenvarieties, L-Functions and Galois Representations, Editors: Burns, Buzzard, Nekovar, Publisher: Cambridge University Press, Pages: 59-120, ISBN: 9780521694155

We axiomatise and generalise the "Hecke algebra" construction of the Coleman-Mazur Eigencurve. In particular we extend the construction to general primes and levels. Furthermore we show how to use these ideas to construct "eigenvarieties" parametrising automorphic forms on totally definite quaternion algebras over totally real fields.

Buzzard K, Calegari F, 2006, The 2-adic eigencurve is proper, *Documenta Mathematica*, Vol: Extra Volume: John H. Coates' Sixtieth Birthday, Pages: 211-232, ISSN: 1431-0643

Coleman and Mazur ask whether the Eigencurve hasany “holes”. We answer their question in the negative for the 2-adicEigencurve of tame level one.

Buzzard K, Calegari F, 2005, Slopes of overconvergent 2-adic modular forms, *COMPOSITIO MATHEMATICA*, Vol: 141, Pages: 591-604, ISSN: 0010-437X

- Author Web Link
- Cite
- Citations: 15

Buzzard K, Kilford LJP, 2005, The 2-adic eigencurve at the boundary of weight space, *COMPOSITIO MATHEMATICA*, Vol: 141, Pages: 605-619, ISSN: 0010-437X

- Author Web Link
- Cite
- Citations: 21

Buzzard K, 2005, Questions about slopes of modular forms, *ASTERISQUE*, Pages: 1-15, ISSN: 0303-1179

- Author Web Link
- Cite
- Citations: 22

Buzzard K, Calegari F, 2004, A counterexample to the Gouvea-Mazur conjecture, *COMPTES RENDUS MATHEMATIQUE*, Vol: 338, Pages: 751-753, ISSN: 1631-073X

- Author Web Link
- Cite
- Citations: 13

Buzzard K, 2004, On p-adic families of automorphic forms, Boston, Modular curves and abelian varieties, Bellaterra, Spain, July 2002, Publisher: Birkhauser Verlag, Pages: 23-44

Buzzard K, 2003, Analytic continuation of overconvergent eigenforms, *JOURNAL OF THE AMERICAN MATHEMATICAL SOCIETY*, Vol: 16, Pages: 29-55, ISSN: 0894-0347

- Author Web Link
- Cite
- Citations: 53

Buzzard K, Stein WA, 2002, A mod five approach to modularity of icosahedral Galois representations, *PACIFIC JOURNAL OF MATHEMATICS*, Vol: 203, Pages: 265-282, ISSN: 0030-8730

- Author Web Link
- Cite
- Citations: 7

Buzzard K, Dickinson M, Shepherd-Barron N,
et al., 2001, On icosahedral Artin representations, *DUKE MATHEMATICAL JOURNAL*, Vol: 109, Pages: 283-318, ISSN: 0012-7094

- Author Web Link
- Cite
- Citations: 37

Buzzard K, 2001, A mod l multiplicity one result, appendix to "Lectures on Serre's Conjectures" by K. Ribet and W. Stein, Arithmetic algebraic geometry, Editors: Conrad, Rubin, Publisher: American Mathematical Society Institute for Advanced Study, Pages: 223-225, ISBN: 9780821821732

Buzzard K, 2001, Families of modular forms, *Journal de Théorie des Nombres de Bordeaux*, Vol: 13, Pages: 43-52, ISSN: 1246-7405

Buzzard K, 2000, On level-lowering for mod 2 representations, *Mathematical Research Letters*, Vol: 7, Pages: 95-110, ISSN: 1073-2780

Buzzard K, Taylor R, 1999, Companion forms and weight one forms, *Annals of Mathematics*, Vol: 149, Pages: 905-919, ISSN: 0003-486X

Buzzard K, 1997, Integral models of certain shimura curves, *Duke Mathematical Journal*, Vol: 87, Pages: 591-612, ISSN: 0012-7094

Buzzard K, 1996, On the eigenvalues of the Hecke operator T-2, *Journal of Number Theory*, Vol: 57, Pages: 130-132, ISSN: 0022-314X

Buzzard K, Hughes C, Lau K, et al., Schemes in Lean

We tell the story of how schemes were formalised in three different ways inthe Lean theorem prover.

This data is extracted from the Web of Science and reproduced under a licence from Thomson Reuters. You may not copy or re-distribute this data in whole or in part without the written consent of the Science business of Thomson Reuters.