A few days ago, I noted the revival of one archaic mathematical practice, namely that of encrypting one's proofs (or announcements). Today, as part of the ongoing Integrated Explicit Analytic Number Theory Network project https://www.ipam.ucla.edu/news-research/special-projects/integrated-explicit-analytic-number-theory-network/ , we found ourselves reviving another archaic piece of mathematical infrastructure: the logarithm table.

These tables, pioneered by Napier in the 17th century, were a mainstay of mathematical computation until eventually supplanted first by calculators and then by modern computers. But we are finding that verifying in Lean that, say, ln 2 is equal to 0.693147 to six decimal places is somewhat fiddly and computationally expensive to formally verify (one has to use a Taylor series with explicit remainder and figure out where to cut off the series).

Eventually we settled on what is basically the 17th century solution, modernized for the era of formal proof verification: the project now sports a file `LogTables.lean` which systematically gathers formally verified calculations of logarithms via a new interval arithmetic package. Similar to a precomputed log table, this file is intended to be typechecked once (as a laborious calculation), and then imported as needed by all other files.

It is a fascinating paradox that cutting edge technology can sometimes make obsolete practices relevant again, albeit with a modern spin. (Yet another example: the capability of current AI tools has revived the in-person class exam, which we had just started to move away from in the COVID era.)