If you pick an answer to this question at random, what are the chances that you will be correct?
- 50%48.3%
- 50%51.7%
584 votesFinal results
3
5
35
Follow
Click to Follow XenaProject
Kevin Buzzard
@XenaProject
Mathematician learning Lean and trying to teach it to others. . Prove a theorem; write a function. #leanprover
Kevin Buzzard’s Tweets
If you're on the post-doc job market and want to come to Imperial to hang out with me, and if you're British, then you're eligible for this heilbronn.ac.uk/about/fellowsh . You spend 50% of your time doing UK government work (whatever that entails) and the other 50% doing what you like.
5
19
Max Zeuner gave an excellent seminar on how he formalized schemes using the univalence axiom:
2
9
52
Chris Birkbeck, lecturer at UEA in Norwich, has funding for a new PhD student to formalise various aspects of the Langlands Program in Lean. Job ad here uea.ac.uk/course/phd-doc , application deadline 27th Nov.
1
15
40
In 2022 plenty of people know the relevant (hard) maths and plenty of people can use Lean, but the number of people who know both is small. So some checks and balances are necessary. The examples github.com/leanprover-com are for people who know some of the maths but not the Lean.
7
Show this thread
OK so Commelin, Topaz et al *claim* to have formalised in Lean the proof of a theorem of Clausen and Scholze saying "some higher Ext groups are 0". But how do we know they didn't cheat by e.g. *defining* the Ext groups to be zero? Topaz explains how here:
2
5
28
Show this thread
Wooah. 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. leanprover-community.github.io/flt-regular/de
4
37
185
This is great (AI discovered the DeepMind algos BTW). Strassen observed that it's possible to multiply two 2x2 matrices together using only 7 multiplications (and as many additions and subtractions as you like). Is it known that it's impossible to do it using only 6?
Quote Tweet
Hmm, this paper recently appeared showing better results than recent results from @DeepMind. If true, it should get an even equivalent media attention. Any ideas? #AI #MachineLearning
2
3
38
This lecture is in Maastricht in Jan 2023. Anyone who knows the answer please let me know before then! Thanks in advance! Here's an easier question: can computers be *creative* in chess or go?
Quote Tweet
14
2
28
The Lean 3 library mathlib made it to 100,000 theorems and 1,000,000 lines of code over the weekend. leanprover-community.github.io/mathlib_stats. . It's just over 5 years old. Wow.
2
37
178
"Why avoid LEM? Then you can prove less theorems!? I want to prove more theorems!"
Hendrik Lenstra (at least according to slideshare.net/brouwerseminar)
16
6
39
Imperial College's maths department just issued their annual post-doc call imperial.ac.uk/jobs/descripti . Typically we get several hundred applications for just a couple of positions so you'll need a little luck, but if you apply then good luck!
1
4
25
Thanks to for pointing out the paper pnas.org/doi/10.1073/pn to me. It explains how the authors got a transformer-based language model to do undergraduate-level mathematics!
2
5
30
An overview of the culmination of the Liquid Tensor Experiment, completed in July 2022 at ICERM.
2
19
55
What was been added to Lean's mathematics library `mathlib` last month? A lot of stuff! leanprover-community.github.io/blog/posts/mon . Kähler differentials, normal closure, Doob's upcrossing estimate and the martingale convergence theorem, the special adjoint functor theorem and much more!
1
9
37
Registration for the interdisciplinary scientific workshop "Creativity in Mathematics and AI" (CMAI 2023) 18-20 January 2023 in The Netherlands, is now possible via aanmelder.nl/cmai/home
read image description
ALT
3
9
17
Show this thread
4
16
Note that there's nothing of any interest here to e.g. a number theorist, other than the news that there are mathematicians out there formalising things like local class field theory, modular forms, Serre's GAGA etc (all necessary prerequisites for FLT) in Lean.
4
23
Show this thread
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.
ma.imperial.ac.uk/~buzzard/xena/
10
32
134
Show this thread
Yes -- Koepke and his colleagues have been working on a similar project for Isabelle.
Quote Tweet
Replying to @XenaProject
There's also this: sketis.net/2019/isabelle-
3
The goal of Patrick's tool isn't to make Lean writing easier, it is a teaching tool whose goal is to make it easier to go from Lean to paper (and then ultimately to do math without Lean). It's for first year mathematics and computing undergraduates.
Quote Tweet
This proof is computer code which compiles. It's written by Patrick Massot. In Lean 4 it will be even better :-)
Show this thread
3
42
More of this stuff at github.com/PatrickMassot/ . Massot has a French version too; he uses it for teaching 1st year undergrads in Orsay.
3
6
40
Show this thread
This proof is computer code which compiles. It's written by Patrick Massot. In Lean 4 it will be even better :-)
18
56
408
Show this thread
Anyone who claims that types and sets are not the same is making an assertion which is evil in the precise sense explained in this nLab article: ncatlab.org/nlab/show/prin
6
1
10
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.
14
12
94
In Lean we define "preprime" to mean "if p=a*b then a=1 or b=1" so the preprimes are 1 and the primes. A bunch of lemmas about primes are also true for preprimes (e.g. p divides xy implies p divides x or y). Similarly "preconnected" is "connected or empty".
1
21
Show this thread
More generally I wonder whether fields should be allowed to be Dedekind domains. This idea was first suggested to me by David Helm. In Lean you really notice that some of the proofs of Dedekind domain things are "if it's a field, then it's obvious. So assume it's not. Then..."
2
9
Show this thread
Do you think it's a mistake that fields are allowed to be principal ideal domains? Is this a bit like allowing 1 to be prime? Geometrically, principal ideal domains are smooth and one-dimensional. Oh, or perhaps a point, if we allow fields.
3
2
32
Show this thread
Guest post on my blog by computing+maths Yale undergraduate Zhangir Azerbayev, about a cool Lean toy he's been making.
14
43
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.
8
21
282
Aww thanks!
Quote Tweet
did i say the Natural Number Game for @leanprover is fantastic? because it is fantastic. ma.imperial.ac.uk/~buzzard/xena/
1
2
17
Don't worry! *He has a Fields Medal!*
9
Show this thread
Borcherds explaining the difference between "the" canonical divisor and "a" canonical divisor. "There are lots of canonical divisors". That clears that up then. Starts at 12 mins.
3
4
38
Show this thread
Composite of injective functions is injective. Proof: compose the injectivity hypotheses! The first is f(a)=f(b) -> a=b and the second is g(f(a))=g(f(b)) -> f(a)=f(b). Lean's unifier figures out which variables you must mean.
read image description
ALT
2
5
47
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.
18
24
335
Show this thread
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
45
371
Show this thread
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.
3
15
207
Show this thread
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
162
Show this thread
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.
92
284
2,230
Show this thread
This year I taught a course about how to formalise undergraduate mathematics, to undergraduate mathematicians. Here's how it went.
20
47
257