Stack Exchange

Kevin Buzzard

London

http://www.ma.imperial.ac.uk/~buzzard

Kevin Buzzard. Algebraic number theorist in London. Interested in formal theorem proving.

My blog aimed at teaching undergraduates to use Lean, a formal proof verification system: https://xenaproject.wordpress.com/

top accounts reputation activity bookmarks subscriptions
Top Questions
126 votes

what mistakes did the Italian algebraic geometers actually make?

ag.algebraic-geometry ho.history-overview asked Mar 26 '10 at 13:26
mathoverflow.net

124 votes

Which mathematical definitions should be formalised in Lean?

big-list proof-assistants lean-theorem-prover asked Sep 21 '18 at 10:34
mathoverflow.net

100 votes

solving $f(f(x))=g(x)$

set-theory gn.general-topology real-analysis fractional-iteration asked Mar 9 '10 at 15:40
mathoverflow.net

71 votes

What are the local Langlands conjectures nowadays, for connected reductive groups over a $p$-adic field?

langlands-conjectures nt.number-theory galois-representations automorphic-forms asked Feb 9 '10 at 12:28
mathoverflow.net

64 votes

Open project: Let's compute the Fourier expansion of a non-solvable algebraic Maass form.

nt.number-theory computational-number-theo langlands-conjectures asked May 5 '10 at 14:30
mathoverflow.net

53 votes

Two (probably) equal real numbers which are not proved to be equal?

real-analysis decidability asked May 7 '19 at 15:01
mathoverflow.net

51 votes

Cauchy reals and Dedekind reals satisfy “the same mathematical theorems”

lo.logic ordered-fields asked Jul 15 '19 at 17:10
mathoverflow.net

49 votes

Erratum for Cassels-Froehlich

books class-field-theory algebraic-number-theory nt.number-theory asked Jan 11 '10 at 15:20
mathoverflow.net

45 votes

Why is the standard definition of cocycle the one that _always_ comes up??

group-cohomology at.algebraic-topology asked Nov 27 '09 at 13:00
mathoverflow.net

42 votes

Automatically solving olympiad geometry problems

lo.logic euclidean-geometry proof-assistants asked Aug 3 '19 at 17:23
mathoverflow.net

1 2 3 4 5 … 7

Top Answers
182
What programming languages do mathematicians use?
mathoverflow.net

121
Proofs shown to be wrong after formalization with proof assistant
mathoverflow.net

112
Extent of “unscientific”, and of wrong, papers in research mathematics
mathoverflow.net

109
Etale cohomology — Why study it?
mathoverflow.net

78
What would you want to see at the Museum of Mathematics?
mathoverflow.net

68
Smooth proper scheme over Z
mathoverflow.net

65
What is the definition of “canonical”?
mathoverflow.net

65
How do I check if a functor has a (left/right) adjoint?
mathoverflow.net

61
What are “perfectoid spaces”?
mathoverflow.net

50
If $2^x $and $3^x$ are integers, must $x$ be as well?
mathoverflow.net

49
Fermat's Last Theorem for Gaussian Integers ( excluding $\mathbb{Z}$ or $i\mathbb{Z}$ )
mathoverflow.net

47
How do you approach your child's math education?
mathoverflow.net

46
What is the difference between PSL_2 and PGL_2?
mathoverflow.net

44
Are there Maass forms where the expected Galois representation is $\ell$-adic?
mathoverflow.net

43
A Game on Noetherian Rings
mathoverflow.net

41
Is it true that, as $\Bbb Z$-modules, the polynomial ring and the power series ring over integers are dual to each other?
mathoverflow.net

41
What are the reasons for considering rings without identity?
mathoverflow.net

40
Tools for the Langlands Program?
mathoverflow.net

40
How did Birch and Swinnerton Dyer arrive at their conjecture?
mathoverflow.net

39
Character table does not determine group Vs Tannaka duality
mathoverflow.net

35
Is “all categorical reasoning formally contradictory”?
mathoverflow.net

34
Integers not represented by $ 2 x^2 + x y + 3 y^2 + z^3 - z $
mathoverflow.net

34
Still Difficult After All These Years
mathoverflow.net

32
How do you select an interesting and reasonable problem for a student?
mathoverflow.net

31
Online, evolving, collaborative foundational text projects
mathoverflow.net

31
Why is one interested in the mod p reduction of modular curves and Shimura varieties?
mathoverflow.net

31
What to do when your research runs into a computationally challenging problem?
mathoverflow.net

28
Why are topological ideas so important in arithmetic?
mathoverflow.net

28
Particular problem solved by solving a more general problem.
mathoverflow.net

28
What makes dependent type theory more suitable than set theory for proof assistants?
mathoverflow.net

1 2 3 4 5 6