[est]

The next natural step would be write down all theorems from kindergarten to undergrad and make them reproduciable with http://leanprover.github.io/

[vixen99]

One could start with the almost 1000 pages of George Shoobridge Carr's a synopsis of elementary results in pure mathematics published in 1837. If someone were to update this book for 2021 I'm curious to know how many pages that might run to.