Not related to anything, but I am amused that the ambiguity of spoken word operator precedence is now defined in a sequence of interest. The sequence injects parentheses and then drops them, $2*5+1 \rightarrow 2*(5+1) = 2*5+2 \rightarrow 2*(5+2)$ etc

Link to documentation is now at doc.sagemath.org/html/en/reference/arithmetic_curves/sage/…

I think this answer can be expanded a bit (perhaps by someone more knowledgeable than myself). Russell and Whitehead continued work on the idea, but about the same time of the second edition of Principia Mathematica, Godel published his papers and that kind of killed the project, with some implications for Hilbert's open problems at the time. (I can't find a good source, but IIRC, Russell continued to work on his theory of classes, or at least revisited the idea a little some years later.)

Now available in Transactions of the AMS: ams.org/journals/tran/0000-000-00/S0002-9947-2019-07881-9/… or DOI doi.org/10.1090/tran/7881

Sorry @AndrejBauer I should have added some context. I was assuming you're aware of the content in the linked answer since you left some comments there. I wasn't really commenting on the content of your answer, just trying to leave a footnote here for other people (like me) not as acquainted with the topic: for anyone interested in further reading on the problem of theorem equivalence, see the many different answers to the question I linked.

"whether two theorems "state the same thing" is a very hard computational problem" -> see When are two proofs of the same theorem really different proofs

Integer factorization is strongly believed not to be NP-complete

Project Gutenberg (edit: a non-profit that exists to enable electronic access to public domain works) has a helpful FAQ about re-releasing works (in the US) without copyright restrictions. The "easy" standard is any edition published before 1923 is always fine, with some exceptions for more recent works. See gutenberg.org/wiki/Gutenberg:Copyright_FAQ and of course, consult a lawyer.