arXiv subjects
Publications and source records attributed to Kevin Buzzard.
Computers have already changed the way that humans do mathematics: they enable us to compute efficiently. But will they soon be helping us to reason? And will they one day start reasoning themselves? We give an overview of recent developments in neural networks, computer theorem provers and large language models.
We discuss how the concept of equality is used by mathematicians (including Grothendieck), and what effect this has when trying to formalise mathematics. We challenge various reasonable-sounding slogans about equality.
A proof is one of the most important concepts of mathematics. However, there is a striking difference between how a proof is defined in theory and how it is used in practice. This puts the unique status of mathematics as exact science into peril. Now may be the time to reconcile theory and practice, i.e. precision and intuition, through the advent of computer proof assistants. For the most time this has been a topic for experts in specialized communities. However, mathematical proofs have become increasingly sophisticated, stretching the boundaries of what is humanly comprehensible, so that leading mathematicians have asked for formal verification of their proofs. At the same time, major theorems in mathematics have recently been computer-verified by people from outside of these communities, even by beginning students. This article investigates the gap between the different definitions of a proof and possibilities to build bridges. It is written as a polemic or a collage by different members of the communities in mathematics and computer science at different stages of their careers, challenging well-known preconceptions and exploring new perspectives.
We discuss the idea that computers might soon help mathematicians to prove theorems in areas where they have not previously been useful. Furthermore we argue that these same computer tools will also help us in the communication and teaching of mathematics.
We tell the story of how schemes were formalised in three different ways in the Lean theorem prover.
Perfectoid spaces are sophisticated objects in arithmetic geometry introduced by Peter Scholze in 2012. We formalised enough definitions and theorems in topology, algebra and geometry to define perfectoid spaces in the Lean theorem prover. This experiment confirms that a proof assistant can handle complexity in that direction, which is rather different from formalising a long proof about simple objects. It also confirms that mathematicians with no computer science training can become proficient users of a proof assistant in a relatively short period of time. Finally, we observe that formalising a piece of mathematics that is a trending topic boosts the visibility of proof assistants amongst pure mathematicians.
We report on a systematic computation of weight one cuspidal eigenforms for the group $Γ_1(N)$ in characteristic zero and in characteristic $p>2$. Perhaps the most surprising result was the existence of a mod 199 weight~1 cusp form of level 82 which does not lift to characteristic zero.
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 \texttt{Sage} readable formats on a webpage created in support of this ongoing project. We explain some of the novel aspects of these computations and what they have uncovered.
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 strategies for making further progress, and examine other related questions.
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-dimensional crystalline representations of G_{Q_p} of slope less than 1, when p > 2.
We develop some of the foundations of affinoid pre-adic spaces without Noetherian or finiteness hypotheses. We give some explicit examples of non-adic affinoid pre-adic spaces (including a locally perfectoid one). On the positive side, we also show that if every affinoid subspace of an affinoid pre-adic space is uniform, then the structure presheaf is a sheaf; note in particular that we assume no finiteness hypotheses on our rings here. One can use our result to give a new proof that the spectrum of a perfectoid algebra is an adic space.
We state conjectures on the relationships between automorphic representations and Galois representations, and give evidence for them.
We explain a highly efficient algorithm for playing the simplest type of dots and boxes endgame optimally (by which we mean "in such a way so as to maximise the number of boxes that you take"). The algorithm is sufficiently simple that it can be learnt and used in over-the-board games by humans. The types of endgames we solve come up commonly in practice in well-played games on a 5x5 board and were in fact developed by the authors in order to improve their over-the-board play.
A Spitalfields Day at the Newton Institute was organised on the subject of the recent theorem that any elliptic curve over any totally real field is potentially modular. This article is a survey of the strategy of the proof, together with some history.
We use the p-adic local Langlands correspondence for GL_2(Q_p) to explicitly compute the reduction modulo p of crystalline representations of small slope, and give applications to modular forms.
In 1987 Serre conjectured that any mod l ("ell", not "1") two-dimensional irreducible odd representation of the absolute Galois group of the rationals came from a modular form in a precise way. We present a generalisation of this conjecture to 2-dimensional representations of the absolute Galois group of a totally real field where l is unramified. The hard work is in formulating an analogue of the "weight" part of Serre's conjecture. Serre furthermore asked whether his conjecture could be rephrased in terms of a "mod l Langlands philosophy". Using ideas of Emerton and Vigneras, we formulate a mod l local-global principle for the group D^*, where D is a quaternion algebra over a totally real field, split above l and at 0 or 1 infinite places, and show how it implies the conjecture.
For p=2 and tame level N=1 we prove that the map from the (Coleman-Mazur) Eigencurve to weight space satisfies the valuative criterion of properness. More informally, we show that the Eigencurve has no "holes"; given a punctured disc of finite slope overconvergent eigenforms over weight space, the center can be "filled in" with a finite slope overconvergent eigenform.
Gouvea and Mazur made a precise conjecture about slopes of modular forms. Weaker versions of this conjecture were established by Coleman and Wan. In this note, we exhibit explicit examples contradicting the full conjecture as it currently stands.