I'm having fun 'peeking in' to what the Lean community is doing (via mostly lurking on their Zulip, but I've perused the source code too). They are genuinely trying to encode huge amounts of mathematics in Lean. 1/n

What makes this effort different than others is that 1. Lean, as a system, has really 'learned' from its predecessors (keep the good, fix some of the bad), 2. there is no philosophical clash between Lean and Math (i.e. the library is unabashedly classical), 2/n

3. there is a strong attempt to make the library uniform and properly compositional.

It is the combination of the three things which makes it the most interesting. 3/n

In this thread, I will make two observations induced by this lurking. Both are about what one can learn about mathematics itself from this exercise. 4/n

First: mathematicians abuse the notion of 'finite set' (and its isomorphism to the natural numbers) a lot. The number of discussions about 'finset' (and 'fintype') and the myriad subtleties about implicit combinatorics that is buried inside normal notation is mesmerizing. 5/n

I'm unfortunately not at the point where I can offer a proper synthesis of the issues, just that it is incredibly obvious that there are a lot. [I saw those first-hand when I tried to do Multicategories in Agda. Nightmare of implicit combinatorics.] 6/n

Second: mathematicians pun a lot. In their notation. A lot. They abuse \\in massively (usually when a structure has a unique carrier, sometimes when it has a unique one of the 'right' type). They also abuse \\subset a lot, when what they truly mean is canonical injection. 7/n

Of course, both those puns are often used together too. This leads to technologies like 'implicit coercions' to try to patch things up. Problem is, mathematicians tend to have enough context to resolve these, but that context isn't so apparent to the tools. 8/n

As far as I can tell, there is a big issue lurking here: both things are ok "in the small", but do not really scale up. Certainly the issue with puns have already been a problem with Coq's mathcomp project. 9/n

Lastly, it is worth pointing out that the Lean project has not been a total slave to traditional mathematical punning. A recent thread by @XenaProject on gcd(0,0) is a great example of unwinding mathematical vernacular into something precise. 10/n

IMHO, there are probably dozens of such 'small insights' about traditional math buried in the Zulip conversations. These really ought to be pulled out and assembled, so that future undergrad math textbooks can benefit from them. 11/n

To me that, that's one of the biggest un-lauded benefits of systemic formalization: systematic clarification of the meaning of various parts of mathematics. 12/n

Personally, I was amazed when reading the Lawvere/Rosebrugh "Sets for Mathematics": I thought I knew and understood basic set theory. But I learned new things from that book about very basic set theory. 13/n

Luckily, the Lean Zulip is all archived (and public). So anyone wishing to do data mining or various sociological reconstructions can do so. Modern communication tools do have some upsides too! 14/14.