Algebraic number theorist, Imperial College London, colourful trousers, currently working on a Lean proof of Fermat's Last Theorem. Proudly funded by EPSRC, part of UKRI.
Kevin Buzzard kbuzzard
Professor of pure mathematics at Imperial College London.
Currently learning about theorem provers.
Highlights
- Pro
Organizations
Pinned Loading
-
leanprover-community/lean-liquid
leanprover-community/lean-liquid Public💧 Liquid Tensor Experiment
-
leanprover-community/lean-perfectoid-spaces
leanprover-community/lean-perfectoid-spaces PublicPerfectoid spaces in the Lean formal theorem prover.
-
ImperialCollegeLondon/FLT
ImperialCollegeLondon/FLT PublicOngoing Lean formalisation of the proof of Fermat's Last Theorem
1,381 contributions in the last year
| Day of Week | April Apr | May May | June Jun | July Jul | August Aug | September Sep | October Oct | November Nov | December Dec | January Jan | February Feb | March Mar | |||||||||||||||||||||||||||||||||||||||||
| Sunday Sun | |||||||||||||||||||||||||||||||||||||||||||||||||||||
| Monday Mon | |||||||||||||||||||||||||||||||||||||||||||||||||||||
| Tuesday Tue | |||||||||||||||||||||||||||||||||||||||||||||||||||||
| Wednesday Wed | |||||||||||||||||||||||||||||||||||||||||||||||||||||
| Thursday Thu | |||||||||||||||||||||||||||||||||||||||||||||||||||||
| Friday Fri | |||||||||||||||||||||||||||||||||||||||||||||||||||||
| Saturday Sat | |||||||||||||||||||||||||||||||||||||||||||||||||||||
Less
No contributions.
Low contributions.
Medium-low contributions.
Medium-high contributions.
High contributions.
More
Contribution activity
April 1, 2025
Created a pull request in leanprover-community/mathlib4 that received 1 comment
chore(RingTheory/DedekindDomain/FiniteAdeleRing): refactor finite adeles
Now we have a general theory of restricted products, we can refactor mathlib's finite adele file, removing the auxiliary results which are unused o…
+90
−406
lines changed
•
1
comment