Kevin Buzzard @XenaProject Twitter profile

Last Seen Profiles

@autorajupiter

@seattleShater

@romerosimone

@surmillon_art

@thelifeofronie

@Lxz668

@WAXDJs

@Chanananwayyy

@Bashar01966850

@5ricc

@vineetspeaks

@officialtwite12

@VasundhraBJP

@EmSiMorales

@_CNSV_

@essaysofesme

@CoachTheobold

@pirogokvp

@Gzk7b1Prhl23612

@Maury_Bs

@tomasz_kacz

@ihoonlvr

@Henai_shokogun

@hiunsuk

@wyk4_1969

@yngxioxidr84443

@Naomi_is_slipy

@yomiii_222

@aqua_cosplay

@akuneko_stage

@pinkticketkr2

@marvinvonhagen

@archiverory

@TheDinoVox

@sasaida0221

@niklasplutte

Kevin Buzzard

@XenaProject

2 years

As a mathematics educator I remain extremely sceptical about assessment via timed exam, perhaps because I've always been suspicious of the idea of measuring mathematical ability by how *quick* you are. The reason they remain is that it's often hard to find an alternative.

80

225

2K

Kevin Buzzard

@XenaProject

10 months

I got a research grant to begin the proof of formalising Fermat's Last Theorem in Lean! The research buys out my teaching and admin for 5 years, which I suspect will not be enough to get it done, but it will certainly be enough to make a big dent in it.

33

148

1K

Kevin Buzzard

@XenaProject

3 months

Fermat's Last Theorem is go!

The Fermat's Last Theorem Project | Lean community blog

Kevin Buzzard discusses the project to prove Fermat's Last Theorem in Lean. Introduction Fermat's Last Theorem (FLT) is the claim that some abstract equation has no solutions in positive integers. Th

leanprover-community.github.io

9

106

455

Kevin Buzzard

@XenaProject

7 months

A team mostly based at DeepMind have created a system which can give accurate natural language solutions to many recent IMO geometry problems . Note that (this kind of) geometry is decidable and e.g. IMO-level number theory is not. But still amazing!

10

107

400

Kevin Buzzard

@XenaProject

2 years

This proof is computer code which compiles. It's written by Patrick Massot. In Lean 4 it will be even better :-)

15

43

371

Kevin Buzzard

@XenaProject

8 months

The Gowers-Green-Manners-Tao proof of Marton's polynomial Freiman-Ruzsa conjecture has now been completely formalised by a team led by Tao. It took three weeks! The project was run on the Lean Zulip; here's Tao's announcement .

3

75

360

Kevin Buzzard

@XenaProject

2 years

Wiles took 7 years to put together a sequence of ideas which proved Fermat's Last Theorem, not 3 hours. Speed was not the crucial factor -- it was insights, which come from a lot of chewing pencils.

6

41

339

Kevin Buzzard

@XenaProject

3 years

Lean makes Nature!

3

83

338

Kevin Buzzard

@XenaProject

3 years

Six months after Peter Scholze challenged the formal proof community to check one of his theorems, he reports on recent developments, and in particular on the efforts of Commelin et al using #leanprover

Half a year of the Liquid Tensor Experiment: Amazing developments

[This is a guest post by Peter Scholze.] Exactly half a year ago I wrote the Liquid Tensor Experiment blog post, challenging the formalization of a difficult foundational theorem from my Analytic G…

xenaproject.wordpress.com

2

91

334

Kevin Buzzard

@XenaProject

2 years

Another thing which concerns me about exams is that they reinforce this macho "I can go faster than you" culture which I think can be unhelpful for women in a class. This is one of the reasons I examined my course by projects, which I think are a much more level playing field.

17

311

Kevin Buzzard

@XenaProject

9 months

Interesting development. Paper at Tao blog post

0

63

301

Kevin Buzzard

@XenaProject

3 years

You know how these AI people say that they're going to get Lean to solve an IMO problem automatically? And we math people know this will never happen because IMO problems are hard. Well according to this new @OpenAI blog post they solved not one but two.

Solving (some) formal math olympiad problems

We built a neural theorem prover for Lean that learned to solve a variety of challenging high-school olympiad problems, including problems from the AMC12 and AIME competitions, as well as two...

openai.com

7

70

297

Kevin Buzzard

@XenaProject

6 months

Tao speaking at the 2024 Joint Math Meetings on machine-assisted proofs. An insightful discussion on various new ways that computers are helping humans to do mathematics.

Terence Tao, "Machine Assisted Proof"

Terence Tao, UCLA, gives the first of three AMS Colloquium Lectures at the 2024 Joint Mathematics Meetings in San Francisco. This lecture is entittled, "Mach...

www.youtube.com

2

84

294

Kevin Buzzard

@XenaProject

8 months

Five million dollars for a computer program that can get gold in IMO: .

AIMO Prize

aimoprize.com

5

60

259

Kevin Buzzard

@XenaProject

2 years

I was taught the pigeonhole principle, as a 1st year undergraduate, by A.R.D. Mathias. He claimed that it was the assertion that if two pigeons were in one hole, then there was one hole which contained two pigeons. He then remarked that this observation could be generalized.

7

19

258

Kevin Buzzard

@XenaProject

8 months

Let Terry Tao take you on a tour of Lean: #leanprover

A slightly longer Lean 4 proof tour

In my previous post, I walked through the task of formally deducing one lemma from another in Lean 4. The deduction was deliberately chosen to be short and only showcased a small number of Lean tac…

terrytao.wordpress.com

1

66

241

Kevin Buzzard

@XenaProject

2 years

1

32

237

Kevin Buzzard

@XenaProject

2 years

This year I taught a course about how to formalise undergraduate mathematics, to undergraduate mathematicians. Here's how it went.

Teaching formalisation to mathematics undergraduates

It’s been a hectic 2022 so far, but August is looking a lot calmer; this is the first of hopefully a few blog posts this month catching up on various things. In this post I want to talk about…

xenaproject.wordpress.com

17

38

233

Kevin Buzzard

@XenaProject

1 year

Ha ha, my PhD student David Ang was teaching Lean about division polynomials in the theory of elliptic curves, and it found a mistake in the literature . The canonical reference seems to be an exercise in Silverman's book, which turns out to be incorrect.

Division polynomials in characteristic two

Let $ E $ be an elliptic curve over a field $ K $ given by a long Weierstrass equation in Jacobian coordinates $ (x : y : z) $ $$ y^2 + a_1xyz + a_3yz^3 = x^3 + a_2x^2z^2 + a_4xz^4 + a_6z^6. $$ What

math.stackexchange.com

3

19

218

Kevin Buzzard

@XenaProject

3 years

Humans proving theorems after being guided to them by AI analysing data. Interesting.

Google DeepMind

@GoogleDeepMind

3 years

A new paper in @Nature details how machine learning was used to make significant new discoveries in pure mathematics by guiding the intuition of some of the world’s top mathematicians from @Sydney_Uni and @OxUniMaths : Paper: 1/

17

613

2K

4

33

204

Kevin Buzzard

@XenaProject

2 years

Johan Commelin has just announced the completion of the formalisation of Peter Scholze's Liquid Tensor Experiment. He revealed the result at "Lean for the curious mathematician", a conference running this week at @ICERM . For details see his blog post .

Completion of the Liquid Tensor Experiment | Lean community blog

We are proud to announce that as of 15:46:13 (EST) on Thursday, July 14 2022 the Liquid Tensor Experiment has been completed. A year and a half after the challenge was posed by Peter Scholze we have f

leanprover-community.github.io

8

58

203

Kevin Buzzard

@XenaProject

3 years

I'm teaching a course on doing maths in theorem provers (using Lean). We're in week 2 and doing some basic analysis. I just made the video proving that the limit of the sum is the sum of the limits. Here it is!

[Formalising math 2022] Section 02: the reals, solutions to sheet 5...

Solutions to reals sheet 5 in the Lean theorem prover.Course notes https://www.ma.imperial.ac.uk/~buzzard/xena/formalising-mathematics-2022/index.htmlCourse ...

www.youtube.com

2

42

201

Kevin Buzzard

@XenaProject

4 years

Peter Scholze poses a nontrivial mathematical challenge for the computer proof verification community.

Liquid tensor experiment

Peter Scholze suggests a mathematical formalization challenge.

xenaproject.wordpress.com

3

53

188

Kevin Buzzard

@XenaProject

2 years

The reason I'm sceptical is that I was always super-quick and noticed very early on that people associated this with being super-smart ("you did well on the IMO / the Cambridge exam system, so therefore you must be a great mathematician"). That's not actually how it works.

2

13

190

Kevin Buzzard

@XenaProject

3 years

Very proud to be a co-author of a published paper with a professional mathematician and four undergrads!

Schemes in Lean

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

www.tandfonline.com

9

16

183

Kevin Buzzard

@XenaProject

2 years

Here are my slides for my talk at the Grothendieck conference at Chapman . I seemed to end up concluding that Grothendieck's concept of equality was kind of difficult to pin down.

18

32

174

Kevin Buzzard

@XenaProject

2 years

Wooah. @RiccardoBrasca and others have proved in Lean that the first case of Fermat's Last Theorem is true for regular primes! In other words, for p regular (a technical condition), there are no integer solutions to a^p+b^p=c^p with a,b,c coprime to p.

3

30

174

Kevin Buzzard

@XenaProject

2 years

Slides for my plenary lecture at the 2022 International Congress of Mathematicians are here .

6

35

165

Kevin Buzzard

@XenaProject

5 years

Waitwaitwait. How did Vice get from "I think there is a non-zero chance that some of our great castles are built on sand" (which I said) to "Number Theorist Fears All Published Math Is Wrong" ??

Number Theorist Fears All Published Math Is Wrong

"I think there is a non-zero chance that some of our great castles are built on sand," he said, arguing that we must begin to rely on AI to verify proofs.

www.vice.com

11

41

166

Kevin Buzzard

@XenaProject

9 months

If anyone wants to watch a pictorial evolution of Tao et al's ongoing Lean formalisation of the Gowers-Green-Manners-Tao proof of the polynomial Freiman-Ruzsa conjecture -- now you can! It's here . The more the proof is formalised, the more it goes green.

2

39

155

Kevin Buzzard

@XenaProject

2 years

The Lean 3 library mathlib made it to 100,000 theorems and 1,000,000 lines of code over the weekend. . It's just over 5 years old. Wow.

2

32

167

Kevin Buzzard

@XenaProject

1 month

The lean community used to do a monthly blog post explaining what math they'd taught Lean recently. Then there was big disruption as the entire code base had to be ported from Lean 3 to Lean 4. This is now long over, and the blog posts have restarted!

This month in Mathlib (May 2024) | Lean community blog

The last Month in Mathlib posts date from before the port started, in November 2022. We apologise for the momentary disappearance. We aim to keep it a monthly occurrence from now on. There were 667 PR

leanprover-community.github.io

0

52

162

Kevin Buzzard

@XenaProject

2 years

Yesterday I tweeted about my recent course which had no final exam, however it was of a rather unconventional nature -- teaching students how to formalise mathematics they already knew in a theorem prover -- so it gave me the chance to tear up the rule book.

2

9

149

Kevin Buzzard

@XenaProject

11 months

The Mandelbrot set and its complement are both connected: Geoffrey Irving just formalised the proof in Lean

3

29

147

Kevin Buzzard

@XenaProject

3 months

Macbeth coherently explains multiple reasons why it's more complicated than "just formalise the lecture notes"

Algorithm and abstraction in formal mathematics

I analyse differences in style between traditional prose mathematics writing and computer-formalised mathematics writing, presenting five case studies. I note two aspects where good style seems to...

arxiv.org

3

18

127

Kevin Buzzard

@XenaProject

3 years

OK so one of the co-founders of Ethereum just announced that they have founded an institute for formalising mathematics at CMU. There will be money for PhD students and post-docs, and we're talking about the kind of maths commonly found in maths departments. More to follow.

Charles Hoskinson

@IOHK_Charles

3 years

The cats out of the bag. Today I got to announce the Hoskinson Center for Formal Mathematics at @CarnegieMellon I donated 20 million dollars to create a permanent center to rewrite the language of math.

689

1K

11K

1

40

146

Kevin Buzzard

@XenaProject

4 years

A blog post in which I attempt to explain to mathematicians (especially young Lean learners) how mathematics is interpreted in type theory.

Mathematics in type theory.

An explanation of how to set up mathematics using universes, types, and terms

xenaproject.wordpress.com

2

34

147

Kevin Buzzard

@XenaProject

4 years

An AI using this GPT thing which folks go on about, has golfed two short proofs in mathlib, Lean's maths library :o So we now have 134 human contributors (including several ICL undergraduates) and 1 computer. Thanks to @jessemhan for letting me know!

[Merged by Bors] - refactor(algebraic_geometry/prime_spectrum): simplify `comap_id`, `comap_comp`...

faster proofs and smaller proof terms Co-authors: lean-gptf, Yuhuai Wu

github.com

2

36

144

Kevin Buzzard

@XenaProject

3 years

Isabelle/HOL has schemes! . The formalisation is due to Bordg, Paulson and Li. In this thread I will try to explain why this is a big deal. 1/n

Grothendieck's Schemes in Algebraic Geometry

www.isa-afp.org

2

40

143

Kevin Buzzard

@XenaProject

3 years

Bit bewildered about whether I'm supposed to be tweeting about my own papers. Anyway, I wrote "What is the point of computers? A question for pure mathematicians" which is supposed to be the companion text to my talk at the forthcoming ICM.

What is the point of computers? A question for pure mathematicians

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...

arxiv.org

6

23

146

Kevin Buzzard

@XenaProject

10 days

DeepMind claiming their system gets a silver medal on 2024 IMO . Note that it took them three days to solve one of the questions, whereas the humans only had 4.5 hours. There was also human intervention translating the questions. But still way beyond SOTA.

AI achieves silver-medal standard solving International Mathematical Olympiad problems

Breakthrough models AlphaProof and AlphaGeometry 2 solve advanced reasoning problems in mathematics

deepmind.google

7

42

247

Kevin Buzzard

@XenaProject

8 months

Oh, weird coincidence! Two flagship Lean math projects finish within 24 hours of each other. This one (Kummer's 1850 proof of FLT for regular primes) took two years, partly because of the upgrade from Lean 3 to Lean 4 during that time. See for more.

Alex Kontorovich

@AlexKontorovich

8 months

A day later, and another major Mathlib project is complete: Fermat's last theorem for "regular" prime exponents! Main contributors: Alex J. Best, Chris Birkbeck, Riccardo Brasca, Xavier Roblot, Eric Rodriguez, Ruben Van de Velde, Andrew Yang Lean FTW!

4

24

157

2

18

133

Kevin Buzzard

@XenaProject

6 months

My post-doc Oliver Nash is working on the classification of semisimple Lie algebras. He's just written a roadmap so if you know some algebra and some Lean (or want to learn) then there are some very concrete targets building towards an important result.

2

33

139

Kevin Buzzard

@XenaProject

8 months

Working on a new level in case Terry Tao or anyone else wants another challenge #LeanProver #LeanLang

3

10

136

Kevin Buzzard

@XenaProject

4 years

Ok so I claim that doing mathematics constructively obscures ideas which, to me at least, feel natural. Let me illustrate with a simple example: a locally open set is open. (1/n)

12

26

131

Kevin Buzzard

@XenaProject

8 months

I gave a talk at EPFL in Lausanne Switzerland: Amongst other things, I explain the extraordinary state of the art when it comes to formalising modern combinatorics (tl;dr: it can now be done in real time).

Abdulle Lecture - Interactive theorem provers : can they help...

The Assyr Abdulle Lecture is a public lecture given periodically by a visitor of the Bernoulli Center for Fundamental Studies.Prof. Assyr Abdulle was a facul...

www.youtube.com

1

17

133

Kevin Buzzard

@XenaProject

5 months

Project going live in April! Let's do this!

New Scientist

@newscientist

5 months

Fermat's last theorem is an infamous puzzle that left mathematicians baffled for centuries. It was finally proven in 1993, but now there is a multi-year plan to do it all over again, using a computer.

4

17

70

2

25

129

Kevin Buzzard

@XenaProject

11 months

Here's a demo of Lean 4 and GPT4 talking about how to prove theorems together. Together they prove 1.8 of them; a human intervened to give a hint in the second one. It's only a demo, so hopefully more to come :-)

Sagredo: automated dialogue between GPT and Lean.

null

www.youtube.com

2

24

131

Kevin Buzzard

@XenaProject

1 year

Me giving a TEDx talk about the usual stuff (theorem provers etc) :

Will machines eat mathematics ? | Kevin Buzzard | TEDxImperialCollege

Will computers be able to do mathematical research, make conjectures, and prove theorems ? Kevin Buzzard gives an overview of the current state of the art of...

www.youtube.com

2

20

127

Kevin Buzzard

@XenaProject

5 months

New journal "Annals of Formalised Mathematics" (diamond open access). It publishes original articles about formalized mathematics and mathematical applications of proof assistants. My PhD students are going to be pleased...

0

22

126

Kevin Buzzard

@XenaProject

3 years

Lol I'm giving a plenary lecture at the ICM Computer games at the International Congress of Mathematicians!

3

16

126

Kevin Buzzard

@XenaProject

4 years

The introduction to my Formalising Mathematics graduate course

Formalising mathematics: an introduction.

An introduction to the TCC course “Formalising Mathematics”

xenaproject.wordpress.com

1

28

123

Kevin Buzzard

@XenaProject

3 months

Anyone interested in using language models to solve mathematical problems should check out the first AIMO progress prize. Unbelievably we already have someone scoring 23/50 on tricky high-school level questions whose answers are an integer between 0 and 999.

AIMO Prize

@AIMOprize

3 months

We welcome D. Sculley, Kevin Buzzard, Leo de Moura, Lester Mackey and Peter J. Liu to the advisory committee for the Artificial Intelligence Mathematical Olympiad Prize! Visit the Prize website for more details:

0

8

28

2

17

121

Kevin Buzzard

@XenaProject

3 years

I spoke at Le Collège de France on Monday on "What is proof?". One of the things I show (starting 21 minutes in, ending 35 minutes in) is that a proof can be thought of as a function; this is not the way a mathematician usually thinks about these objects.

4

20

121

Kevin Buzzard

@XenaProject

2 years

I gave a talk at AITP yesterday on the idea of formalising Fermat's Last Theorem in a theorem prover. I think it's now possible, it will just take a long time. Several people on Twitter have asked to see the slides, which summarize the state of the art.

7

26

119

Kevin Buzzard

@XenaProject

9 months

Thanks to Bhavik Mehta for writing a Xena Project blog post on his work formalising the recent breakthrough bounds in Ramsey numbers by Campos, Griffiths, Morris, and Sahasrabudhe. Formalising modern research mathematics in real time

Formalising modern research mathematics in real time

(This is a guest post by Bhavik Mehta) On March 16, 2023, a paper by Campos, Griffiths, Morris, and Sahasrabudhe appeared on the arXiv, announcing an exponential improvement to the upper bound on R…

xenaproject.wordpress.com

4

23

109

Kevin Buzzard

@XenaProject

2 years

Video for my plenary lecture at the 2022 International Congress of Mathematicians is up on YouTube! . The IMU has had a *nightmare* organising a hybrid ICM since they pulled out of Russia. Congratulations and thanks to them for getting this up so quickly.

Kevin Buzzard: The rise of formalism in mathematics

null

www.youtube.com

1

19

112

Kevin Buzzard

@XenaProject

3 months

Wooah, GPT-4o apparently gets 7/10 on the ten training questions on the AI-MO progress prize. Not bad going!

AI Mathematical Olympiad - Progress Prize 1

Solve national-level math challenges using artificial intelligence models

www.kaggle.com

5

21

111

Kevin Buzzard

@XenaProject

2 years

I think it may come as a surprise to many "establishment mathematicians" (for whom the answer to "is ℕ = ℤ?" is probably "obviously no") to see that there are 80+ people out there, some of whom know what they're talking about, who claim that ℕ = ℤ is true. Why? A 🧵. 1/n

Kevin Buzzard

@XenaProject

2 years

Does ℕ = ℤ ?

14

1

18

6

21

110

Kevin Buzzard

@XenaProject

4 years

Hey algebra Twitter! Imperial undergraduate Kenny Lau just found a cool oversight in the proof of the Artin-Tate lemma in Atiyah--Macdonald, when formalising it in Lean. Of course the proof can be fixed. How to justify "each elt of C is a lin comb of the y_i with coeffts in B_0"?

6

21

109

Kevin Buzzard

@XenaProject

3 years

Interesting experiment by Patrick Massot. He's written a limited controlled natural language for proofs in Lean -- examples of proofs here . These are accepted by Lean's kernel. The parsers doing the work are here

4

18

110

Kevin Buzzard

@XenaProject

3 years

Random Fermat's Last Theorem observation: the bridge between analysis and algebra in it is nonconstructive. 🧵

2

14

105

Kevin Buzzard

@XenaProject

3 months

In just under 24 hours I'll be giving the VaNTAGe seminar during which I'll formally open the Lean Fermat's Last Theorem github repo!

VaNTAGe math

VaNTAGe started in January 2020, as one of the first international virtual seminars about number theory and arithmetic geometry (NT&AG). The seminar provides open access to world class mathematics,...

sites.google.com

2

13

107

Kevin Buzzard

@XenaProject

4 months

Great: Wiles' work doesn't deal with this case so we need it for the FLT project. I really like the idea of crowdsourcing a mathematical proof. The project hasn't even started yet but 6 undergraduates at Imperial have already contributed.

Pietro Monticone

@PietroMonticone

4 months

My colleagues and I have almost finished the formalisation of Fermat’s Last Theorem for exponent 3 in @leanprover . We‘ll port it in Mathlib as soon as we can so it could be used in the FLT project. For those interested, here is our @GitHub repository: .

5

12

63

3

14

103

Kevin Buzzard

@XenaProject

3 years

Ken Lee and Joseph Hua, two undergraduates at Imperial, have made a HoTT game! The main objective is to prove π₁(S¹)=ℤ. It's written in cubical agda. Instructions on how to play are here . Remark: on ubuntu linux I installed atom and it all just worked.

2

23

104

Kevin Buzzard

@XenaProject

1 year

Mura Yakerson is making videos explaining K-theory! With some friends she's making a series of videos called "K-theory Wonderland" on her YT channel. Here are the first few

Something from Nothing

This piece of art, made by Jeremiah Heller, is a true fairytale taking place in K-theory Wonderland!More about this video: https://youtu.be/tqbhAITEDb0Math p...

www.youtube.com

1

19

100

Kevin Buzzard

@XenaProject

1 year

Sophie Morel has formalised the first half of her 2019 joint paper in Lean 4. It took her a month; she had 0 Lean 4 experience when she started (but some Lean 3 experience). The formalisation is here . Welcome aboard Sophie!

GitHub - smorel394/TS1

Contribute to smorel394/TS1 development by creating an account on GitHub.

github.com

3

8

97

Kevin Buzzard

@XenaProject

8 months

Lean Together 2024: free online conference 9-12 Jan 2024. More info at . Talks about using Lean for maths, for software verification, UI features etc. Speakers will range from beginners to experts. Discussions, socials etc.

Home

A meeting all about Lean

leanprover-community.github.io

1

33

100

Kevin Buzzard

@XenaProject

6 months

Aperiodic monotiles coming to Lean, by Joseph Myers, one of the authors of the original papers:

GitHub - jsm28/AperiodicMonotilesLean: Lean formalization of aperiodic monotiles papers (staging...

Lean formalization of aperiodic monotiles papers (staging repository for material not yet in mathlib) - jsm28/AperiodicMonotilesLean

github.com

1

16

98

Kevin Buzzard

@XenaProject

7 months

A chat about some of the achievements of the Lean community in 2023, and what we have to look forward to in 2024:

Lean in 2024

A huge amount happened in the Lean theorem prover community in 2023; this blog post looks back at some of these events, plus some of what we have to look forward to in 2024. Modern mathematics I pe…

xenaproject.wordpress.com

1

19

97

Kevin Buzzard

@XenaProject

2 years

Happy to report that Bloom went on to learn Lean this year and, together with Bhavik Mehta, has now formalised his proof in Lean (including formalising the Hardy-Littlewood circle method), finishing before he got a referee's report for the paper ;-)

Thomas Bloom

@thomasfbloom

3 years

Happy to report progress on this! The answer is yes: a set of integers of positive density must contain distinct n_1,...,n_k such that 1/n_1+...+1/n_k=1.

9

47

263

1

22

96

Kevin Buzzard

@XenaProject

2 years

Recently I learnt something which is presumably well-known: spaces of atoms/coatoms have geometry. Or possibly topology -- I think I no longer know the difference :-/ Examples range from projective spaces to Stone-Cech compactifications to affine varieties. Let me explain. 1/n

4

21

99

Kevin Buzzard

@XenaProject

4 years

EPSRC fund formalisation of mathematics! Possibly for the first time? My New Horizons grant to start digitising the Langlands program got funded! Post-doc ad will be out in the new year.

Imperial College London

@imperialcollege

4 years

"The projects announced today...will no doubt stimulate breakthroughs in knowledge that will lead to longer-term innovations with societal impact" The @EPSRC has awarded 13 of our academics new grants to undertake ‘adventurous and high-risk research'

1

4

17

7

10

96

Kevin Buzzard

@XenaProject

3 years

Congratulations to Imperial mathematics undergrad Kexing Ying whose proof of the Radon-Nikodym theorem just hit mathlib! Well done Jason 🎉

measure_theory.decomposition.radon_nikodym - mathlib3 docs

Radon-Nikodym theorem: “THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. ”This file proves the Radon-Nikodym theorem. The Radon-Nikodym…

leanprover-community.github.io

1

15

95

Kevin Buzzard

@XenaProject

3 years

What's the next equation in this sequence:

11

2

91

Kevin Buzzard

@XenaProject

2 months

Loving this, from p49 of Halmos' autobiography "I want to be a mathematician" (p49).

2

9

96

Kevin Buzzard

@XenaProject

2 years

If φ:G -> H is a group hom then G/ker(φ) is "canonically" isomorphic to im(φ). We mathematicians are so desperate for this to be "the first isomorphism theorem" but part of the content of Emmy Noether's result is the *definition* of a map G/ker(φ)->im(φ); the theorem comes later.

6

7

90

Kevin Buzzard

@XenaProject

2 years

The reason types are the same thing as sets is that the category of types is equivalent to the category of sets. Everything else is just an implementation detail.

10

8

88

Kevin Buzzard

@XenaProject

8 months

How long will the little blue guy last? :-)

3

7

86

Kevin Buzzard

@XenaProject

2 years

Marking 1st year exam scripts. One question: "give, without proof, a sequence a1,a2,... of irrationals such that for every real x there's a subsequence converging to x". Tricky answers so far: a(n)=tan(n) [yes], a(n)=n*sin(n) [yes I think] but now faced with a(n)=e^n*sin(n) 🤔

15

2

86

Kevin Buzzard

@XenaProject

3 years

PhD position available in the Netherlands to work with Freek Wiedijk on beginning the long journey towards a fully formalised proof of Fermat's Last Theorem. More info at .

4

18

87

Kevin Buzzard

@XenaProject

2 years

(generated by @RiccardoBrasca ): Proof of the Clausen-Scholze theorem on vanishing of certain higher Exts in the category of condensed abelian groups, as understood by a computer:

8

10

87

Kevin Buzzard

@XenaProject

4 years

I just saw a computer find a (formally verified) proof that if G is a group and a,b in G satisfy abab^2=1 then ab=ba. It's not hard to prove, but until about 2 minutes ago I thought it required some insight. @chrishughes244 made a Lean tactic following @AndyPutmanMath 's notes.

3

7

83

Kevin Buzzard

@XenaProject

4 years

2020 IMO problem demolished in under 20 lines in Lean by Joseph Myers:

3

15

81

Kevin Buzzard

@XenaProject

2 years

Happy 5th birthday mathlib, Lean's mathematics library 🎂.

1

7

83

Kevin Buzzard

@XenaProject

2 years

Massot, van Doorn and Nash have turned a sphere inside-out in Lean! They formalised a modern proof of Smale's old result that you can evert a sphere (i.e., turn it inside out, allowing it to pass through itself but not allowing creasing or tearing). 1/3

1

27

83

Kevin Buzzard

@XenaProject

2 years

Article in current New Yorker about Grothendieck:

0

21

82

Kevin Buzzard

@XenaProject

3 years

The Lean prover community now has a blog! It discusses the ongoing progress of Lean's mathematics library `mathlib` and the papers which are coming from it. Its most recent post is Imperial's own (UG) Jason Ying talking about his work on measure theory.

Lean community blog

leanprover-community.github.io

0

17

81

Kevin Buzzard

@XenaProject

2 years

Gardam's disproof of Kaplansky's unit conjecture was published in the Annals of Mathematics in 2021 and has been formalised in Lean by Siddhartha Gadgil and Anand Rao Tadipatri here . Cutting edge maths formalised in "real time".

3

20

81

Kevin Buzzard

@XenaProject

6 months

Kontorovich-Tao formalising PNT and more in Lean. I'll need the Cebotarev density theorem for FLT so this is a very welcome development! If you have worked through Mathematics In Lean and want to join in, the blue nodes are the ones where you can contribute.

Alex Kontorovich

@AlexKontorovich

6 months

Terry Tao and I are pleased to announce the "Prime Number Theorem and Beyond" project, which you can find here: with blueprint here: and dedicated stream in the Leanprover Zulip chat. The initial goal is to get the Prime Number

13

157

877

0

10

79

Kevin Buzzard

@XenaProject

2 years

woo -- is now public! Go ask your questions about Lean/Coq/Agda/Isabelle/all the rest of them there!

Proof Assistants Stack Exchange

Q&A for mathematicians and computer scientists who develop and use proof assistants

proofassistants.stackexchange.com

1

34

78

Kevin Buzzard

@XenaProject

3 years

Lean's Mathlib slowly but surely continues to eat mathematics. This month: integral schemes are reduced and irreducible, schemes are sober, Tietze's extension theorem, the Banach-Steinhaus theorem, martingales and super/submartingales, and more.Details at

3

16

80

Kevin Buzzard

@XenaProject

1 year

The Lean Focused Research Organization is a new nonprofit dedicated to advancing the Formal Mathematics revolution. You can read about Focused Research Organizations here . Will be very interesting to see what comes out of this.

2

16

78

Kevin Buzzard

@XenaProject

4 years

Funny proof of infinitude of primes via Myhill-Nerode theorem. For natural n>=1, the language L_n := "words in letters {a,b} with number of a's - number of b's = multiple of n" is regular, but the union over all p of L_p is not so can't be a finite union.

Infinitude of Primes Using Formal Language Theory

Formal languages are sets of strings of symbols described by a set of rules specific to them. In this note, we discuss a certain class of formal languages, called regular languages, and put...

arxiv.org

4

17

76

Kevin Buzzard

@XenaProject

2 years

Brief round-up of some of the main achievements in the Lean community in 2022.

Lean 2022 round-up

A brief survey post containing some of the things which happened in the Lean community in 2022. The Liquid Tensor Experiment In December 2020, Fields Medallist Peter Scholze challenged the formal c…

xenaproject.wordpress.com

0

10

76

Kevin Buzzard

@XenaProject

3 years

You can now play The HoTT Game without having to install cubical agda! 😀Go to , click "new agda session" and then the second icon ("read an existing file into an emacs buffer") and choose an agda file in the TheHoTTGame directory!

0

13

78

Kevin Buzzard

@XenaProject

3 years

I was taught as a maths undergraduate at the University of Cambridge that the quotient of a set by an equivalence relation was a set of sets of things. Nowhere did they ever make it clear that this was just an implementation issue.

3

0

77

Kevin Buzzard

@XenaProject

2 years

Just a fully formalised proof of Fermat's Last Theorem to go then...

Freek Wiedijk 🎲

@freekwiedijk

2 years

The 99th theorem has been formalized (by John Harrison in HOL Light)! 🎉🥳🍾

2

8

55

4

6

74

Kevin Buzzard

@XenaProject

7 months

Discussion of the AlphaGeometry paper on the Lean Zulip chat . Heather Macbeth and Joseph Myers point out a couple of instances where the computer only solves a weakened version of the IMO problem, or does not give a 7/7 soln. But still clearly SOTA :-)

Kevin Buzzard

@XenaProject

7 months

A team mostly based at DeepMind have created a system which can give accurate natural language solutions to many recent IMO geometry problems . Note that (this kind of) geometry is decidable and e.g. IMO-level number theory is not. But still amazing!

10

107

400

2

6

74

Kevin Buzzard

@XenaProject

3 years

Thomas Skrivnan has been working on a Lean 4 library for scientific computation. When Lean 4 has a maths library we will be able to prove theorems about the iteratively-generated solutions he has for differential equations (for example error bounds).

GitHub - lecopivo/SciLean: Scientific computing in Lean 4

Scientific computing in Lean 4. Contribute to lecopivo/SciLean development by creating an account on GitHub.

github.com

3

11

74