Highlights of 2024?

Stream: general

[Matthew Ballard]

As part of the last #general > Mathlib community meetings people offered their views on highlights from the past year for the Lean Community. Below is a(n AI) summary from the transcript.

1. Lean for the Curious Mathematician Workshop:
   • Successful event held in Luminy with ~80 participants, including members of the Coq community.
   • Positive engagement and visibility in France.

2. Category Theory and Homological Algebra:
   • Joel’s significant contributions directly in Mathlib were noted as exceptional achievements.

3. Semisimple Lie Algebras:
   • Progress on the classification and root system work, with expectations for completion soon.

4. PR Activity Milestone:
   • October 2024 marked the first month with over 1,000 pull requests merged.

5. Technical Debt and Refactoring:
   • Notable strides in tracking and reducing technical debt.
   • Improvements to morphism spaces for concrete categories.

6. AI and AlphaProof Success:
   • Mathlib’s foundational role in enabling DeepMind’s AlphaProof was recognized.

7. Manifold Integration:
   • Significant progress by Sebastien G. on integrating analytic and smooth manifolds.

8. Differential Geometry Work:
   • Advances in differential forms and developments in De Rham cohomology were achieved.

9. Annals of Formalized Mathematics:
   • Launch of the journal marks a key milestone, with the first issue expected soon.

10. Community Growth:
    • Increased engagement, teaching courses, and “hidden” Lean communities emerging worldwide.

[Matthew Ballard]

I am sure we missed many great things. It would be nice to add/discuss them here and them here. We can then condense the final product into something more sharable, like a blog post.

[Matthew Ballard]

Please add your highlights!

[Edward van de Meent]

Matthew Ballard said:

PR Activity Milestone:
• October 2024 marked the first month with over 1,000 pull requests merged.

i guess the recent attainment of 20000 PRs total is a nice mention too

[Edward van de Meent]

curiously, june 2023 nearly was the milestone month, falling short by 1 commit

[Marcus Rossel]

My highlights were basically all things @Joachim Breitner worked on: improved termination checking, better equation generation for functions, and functional induction!

[Edward van de Meent]

it seems that gpt missed the queueboard from the transcript

[Patrick Massot]

I would definitely add @Julian Berman bringing lean.nvim at a level where many people can now use it as their primary Lean authoring tool.

[Filippo A. E. Nuccio]

I would like to add Lean Search as a great tool that saw the light of the day in 2024.

[David Loeffler]

I'd like to suggest two more candidates for this list (both specifically about Mathlib, rather than Lean in general)

Firstly, I think the new deprecation system that Mathlib has adopted – so lemmas don't just disappear without warning overnight – is a huge step forward, substantially reducing, although far from eliminating, the frustrations caused to downstream users by the very frequent rate of changes to fundamental parts of the library. (I hope I've remembered accurately that this came in 2024 and not earlier!)

Secondly, at risk of self-advertising (since I had a substantial role in the project), I think that the formalisation by Michael Stoll of Dirichlet's theorem on primes in arithmetic progressions should count among the highlights of 2024. I feel that Dirichlet's theorem is a wonderful example of very "high technology" mathematics (complex analysis, Fourier transforms, Hilbert spaces, ...) being used to prove a theorem whose statement is really very simple; and the fact that mathematics of this technical complexity can be formalised within Mathlib shows how far the project has come.

[Mario Carneiro]

I feel like it is worth noting though that dirichlet's theorem was proved in lean in 2019

[Johan Commelin]

But that wasn't "specifically about Mathlib" but rather "Lean in general", right?

[Mario Carneiro]

yes, it's fair to say that this theorem was not proved using (much) mathlib

[Mario Carneiro]

did we ever get that proof that the real numbers are unique in mathlib?

[Mario Carneiro]

that was the only thing standing in the way of having PNT in 2019 as well

[David Loeffler]

I apologise, I wasn't aware that Dirichlet had been proved as part of Mario's project (although I knew he had done PNT). Mario, which proof of Dirichlet did you formalise back then? Was it the L-functions proof, or something more "elementary" (whatever that means)?

[Mario Carneiro]

both PNT and Dirichlet used "elementary methods"

[David Loeffler]

Indeed; which ones?

[Mario Carneiro]

the Erdos-Selberg identity is the main lemma

[Mario Carneiro]

I've been pretty quiet wrt PNT+ because I realize that the methods are almost completely disjoint and mathlib wants the analysis that comes with the L-functions approach anyway

[Sébastien Gouëzel]

It may be worth pointing out that this proof wasn't done in Lean, but in Metamath, and that Mario got it in Lean thanks to a transfer tool.

[Mario Carneiro]

but it is proved wrt lean axioms only

[Sébastien Gouëzel]

Sure, in the end it's a pure Lean statement, with the most unreadable possible proof :-)

[Mario Carneiro]

(it's not actually that unreadable, but I know people want to think of it that way)

[Sébastien Gouëzel]

Just copying the beginning of one of the files:

import .set5

namespace mm0

theorem dvmptfsum {v2 : wff} {v3 v4 : setvar → setvar → «class»} {v5 v6 : «class»} {v7 v8 : setvar → setvar → «class»} {v9 : «class»}
  (v10 : ∀ v0 v1, ⊦ wceq (v7 v0 v1) (co (v8 v0 v1) v5 crest))
  (v11 : ∀ v0 v1, ⊦ wceq (v8 v0 v1) (cfv ccnfld ctopn))
  (v12 : ⊦ wi v2 (wcel v5 (cpr cr cc)))
  (v13 : ∀ v0 v1, ⊦ wi v2 (wcel v9 (v7 v0 v1)))
  (v14 : ⊦ wi v2 (wcel v6 cfn))
  (v15 : ∀ v0 v1, ⊦ wi (w3a v2 (wcel (cv v1) v6) (wcel (cv v0) v9)) (wcel (v3 v0 v1) cc))
  (v16 : ∀ v0 v1, ⊦ wi (w3a v2 (wcel (cv v1) v6) (wcel (cv v0) v9)) (wcel (v4 v0 v1) cc))
  (v17 : ∀ v1, ⊦ wi (wa v2 (wcel (cv v1) v6)) (wceq (co v5 (cmpt (λ v0, v9) (λ v0, v3 v0 v1)) cdv) (cmpt (λ v0, v9) (λ v0, v4 v0 v1)))) :
  ⊦ wi v2 (wceq (co v5 (cmpt (λ v0, v9) (λ v0, csu v6 (λ v1, v3 v0 v1))) cdv) (cmpt (λ v0, v9) (λ v0, csu v6 (λ v1, v4 v0 v1)))) :=
let v73 := λ v0, @«0cnd» (wa v2 (wcel (cv v0) v5)) in
let v82 := λ v19 v20, @mpan (wss (cv v19) (cun (cv v19) (csn (cv v20)))) (wss (cun (cv v19) (csn (cv v20))) v6) (wss (cv v19) v6)
  (@ssun1 (cv v19) (csn (cv v20)))
  (@sstr (cv v19) (cun (cv v19) (csn (cv v20))) v6) in
let v95 := λ v19 v20, @simpll v2 (wn (wcel (cv v20) (cv v19))) (wa (wss (cun (cv v19) (csn (cv v20))) v6) (wceq (co v5 (cmpt (λ v0, v9) (λ v0, csu (cv v19) (λ v1, v3 v0 v1))) cdv) (cmpt (λ v0, v9) (λ v0, csu (cv v19) (λ v1, v4 v0 v1))))) in
let v99 := λ v19 v20 v18, @ad3antrrr v2 (wcel v6 cfn) (wn (wcel (cv v20) (cv v19))) (wss (cun (cv v19) (csn (cv v20))) v6) (wcel (cv v18) v9)
  v14 in
let v100 := λ v19 v20 v18, @ad2antlr (wss (cun (cv v19) (csn (cv v20))) v6) (wss (cv v19) v6) (wa v2 (wn (wcel (cv v20) (cv v19)))) (wcel (cv v18) v9)
  (v82 v19 v20) in
let v109 := λ v1 v18, @nfv (w3a v2 (wcel (cv v1) v6) (wcel (cv v18) v9)) in
let v110 := λ v1 v18, @nfcsb1v (cv v18) (λ v0, v3 v0 v1) in
let v111 := λ v1 v18, @nfel1 (λ v0, csb (cv v18) (λ v0, v3 v0 v1)) cc
  (v110 v1 v18) in

Everyone can decide for himself if it looks unreadable or not. Personally, it reminds me a little bit of the source code of the Google homepage :-)

[Sébastien Gouëzel]

And I find it amazing both that Mario could produce these files from the metamath version of the proof, and that Lean can swallow them like a piece of cake.

[Mario Carneiro]

this is basically equivalent to looking at pp.all proofs

[Mario Carneiro]

I had to actively avoid notations and such in the generated files to avoid lean getting confused

[Ruben Van de Velde]

I'm both amazed by the generated proof and glad we have the lean-first project :)

[Mario Carneiro]

it's very difficult to generate lean files that reliably elaborate implicit arguments without weird slowdowns

[Mario Carneiro]

I recently updated this project to work on latest lean 3, in preparation for mathport. If I were to do a lean 4 version I would definitely not generate source code. I'm pretty sure lean 4 has significantly regressed on this kind of workload - it would probably take ages to do linting or some other random thing

[Mario Carneiro]

Also, when looking at those files, consider that doing the same thing for lean 3 mathlib would be significantly worse (the terms are much bigger and basically can't even be printed, and notations are also broken or missing in many cases)

[Mario Carneiro]

So I really think it's a bit of an unfair comparison to just look directly at the dump and complain that it isn't very clear, when none of the tooling which exists to make it clear is being used

[Mario Carneiro]

just like anything else, it's just a matter of putting in enough time and effort to make the difference between "widgets in the infoview" and "reading .olean files in a hex editor"

[Johan Commelin]

Mario Carneiro said:

did we ever get that proof that the real numbers are unique in mathlib?

Yes! docs#LinearOrderedField.uniqueOrderRingIso and docs#instConditionallyCompleteLinearOrderedFieldReal

[Yaël Dillies]

(it's been a while even. Alex Best and I did that back in 2021/2022)

[Kevin Buzzard]

The thing we never got was that Lean's log was equal to Metamath's log, because we never had some fancy characterisation of log which didn't say words like "continuous".

[Mario Carneiro]

I don't think that is a problem, because they should have similar definitions. Log is the inverse of exp, and exp is the sum of an infinite series, and infinite series have unique solutions when they exist

[Mario Carneiro]

it all comes down to epsilon-delta definitions and then it's axiomatic real numbers

[Mario Carneiro]

so while nonzero work it seems relatively clear how to do it, as long as lean has theorems like "exp z = exp w iff z - w is a multiple of $2\pi i$"

[Kevin Buzzard]

and then you have to check that Lean pi = Metamath pi?

[Kevin Buzzard]

Matthew Ballard said:

2. Category Theory and Homological Algebra:
   • Joel’s significant contributions directly in Mathlib were noted as exceptional achievements.

Richard Hill and I are running a Clay workshop on class field theory in July (announcement soon); class field theory is an essential prerequisite for FLT. Richard's question here came from developing some of the theory which we'll need for this, and it was wonderful to see that Joel's work from earlier this year enabled us to answer it immediately. What I'm trying to say is that Joel's work has applications well beyond abstract category theory.