That'll be useful for Fermat

hal.science/hal-04546712

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.

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

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

It's great to see this. Lean is of course also developing a theory of schemes, but I think that if development occurs in more than one system then users of both systems have potential to learn from the other development.

Something I learnt from David Loeffler last week: The mathematician's zeta function isn't defined at s=1, but in Lean the philosophy is to define it there anyway as a junk value. Turns out that nobody knows the actual *value* of zeta(1) in Lean! It may well involve gamma.

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

github.com/jsm28/Aperiodi…

Note the evolution of the blueprint software: light green means 'done', and dark green means 'done, as are all prerequisites'. Anyone who knows some basic analytic number theory and some Lean is welcome to join in; make yourself known on the Lean Zulip leanprover.zulipchat.com

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. youtube.com/watch?v=AayZuu…

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.

My post-doc Oliver Nash is working on the classification of semisimple Lie algebras. He's just written a roadmap github.com/orgs/leanprove… 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.

A chat about some of the achievements of the Lean community in 2023, and what we have to look forward to in 2024: xenaproject.wordpress.com/2024/01/20/lea…

Discussion of the AlphaGeometry paper on the Lean Zulip chat leanprover.zulipchat.com/#narrow/stream…. 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 :-)

Imperial maths is hiring. Even better: 'Preference may be given to candidates with expertise in proof formalisation.'

imperial.ac.uk/jobs/descripti…

Formalisation of Mathematics: A Workshop for Women and Mathematicians of Minority Gender . Organised at ICMS at the end of May. Deadline for registration is 26th Feb. See icms.org.uk/Formalisation .

A team mostly based at DeepMind have created a system which can give accurate natural language solutions to many recent IMO geometry problems nature.com/articles/s4158… .

Note that (this kind of) geometry is decidable and e.g. IMO-level number theory is not. But still amazing!

Lean Together 2024, a free online conference about the Lean theorem prover and programming language, will be held 9-12 January, 2024. More details and registration are available at leanprover-community.github.io/lt2024/

I gave a talk at EPFL in Lausanne Switzerland:
youtube.com/watch?v=fwfd8_…

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

Rumours of its demise were highly exaggerated: the London School of Geometry and Number Theory, a joint PhD program between Imperial/Kings/UCL, is back! lsgnt-cdt.ac.uk Applications are open, closing end of Dec. Come and do your PhD in London surrounded by smart people.

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