Read Part 1 here.

You’ve heard calls for new literacy before

If you lived though the 2000s and 2010s, this analogy may sound familiar. The concepts of “numeracy” (numerical literacy) and “code literacy” were both popular and advocated during that time.

Numeracy is, to quote Wikipedia, “the ability to understand, reason with, and apply simple numerical concepts”. This includes things like being able to do mental math in the grocery store, understanding the difference between a millionaire and a billionaire, and that conjunctions are less probable than their individual parts.

The “learn to code” movement was, to quote Wikipedia again, “a series of public influence campaigns during the 2010s that encouraged the development of computer programming skills in an economy increasingly centered on information technology”. These skills are often referred to as “code literacy”. The movement was largely a job retraining program, but it was also considered important for the general public to understand how computers and software work, and there are many non-software-development jobs where a basic ability to code is useful.

Many nonprofits and governmental policies were created to measure and increase both types of skills among the general population. I think these are both good things to increase on the margin. But it’s not clear to me that we should aim for a particularly large fraction of the population to have them (aside from basic numeracy, which is as important as reading).

I claim that my call for Lean literacy is fundamentally different for two reasons, and a much better match for the original concept of literacy.

A funny thing about language is that we have two totally different systems for it; a spoken one and a written one. Everyone learns the spoken modality as a natural and necessary part of healthy human development. Spoken language is at least as old as Homo sapiens (~300 thousand years old).

Written language though, was invented. It’s only about 5 thousand years old. And so it must be much more deliberately taught. But what you are teaching is not a bunch of new concepts; you’re just teaching the person to recognize the correspondence between a modality they already know and a new modality.

This is emphatically not the case for numeracy and code literacy. Those are both large collections of arguably unnatural concepts. They are also, I would claim, not concepts that everyone can learn. In contrast, it does seem that essentially everybody can learn to read.

Reading Lean code is obviously a far more niche skill than any of those. But within the population of mathematicians, Lean code is just a different modality of representing the same body of concepts that all mathematicians are intimately familiar with. We could even have a hypothetical world where Lean code is the only modality of communicating mathematics, in the same way that we could hypothetically have a world where humans never spoke, only wrote.

Because it is only a different modality of representing familiar concepts, I have no doubt that all mathematicians could learn to read Lean.

Mathematicians already do this all the time

In fact, I’d claim that mathematicians already know several different ways of representing mathematical concepts.

First is the fact that all mathematics can be expressed in English (and any other natural language a mathematician may speak). Math papers are, despite their reputations, mostly written in natural language, with the symbolic expressions interspersed. If pressed, mathematicians can read the whole thing out loud.

When a mathematician writes down their theorem statement, the amount of it that is in symbols versus languages is a matter of stylistic preference. This is especially true at the level of the logical structure of the theorem (saying “if and only if” versus ⇔, or “for all” rather than ∀) but people also commonly say things like “f and g commute” rather than “f∘g = g∘f”. They also often say it both ways, just to be clear. And complicated properties are frequently given single-word adjective names, which are then used fluidly amongst the symbols.

There’s also the matter of different notational systems for different subfields. Derivatives can be denoted with d/dx or x’. Tensor calculus and differential geometry can make the same equation look unrecognizably different. Many logical statements about objects with certain properties can be alternatively expressed as unions and intersections over the sets of objects with those properties. Is this a product of conditional probability distributions or a compositions of kernels or a Bayes net diagram? Doesn’t matter, mathematicians have it handled.

And then there is LaTeX. Not many people prefer to read and write statements like \frac{d}{dx} \int_a^x f(t)\,dt = f(x), but everyone understands that it’s necessary to participate in the standards of the global mathematics community, and over the last 30 years or so essentially everyone has transitioned to using it.

[Part 3 coming soon]