This is cool and I looked into this many years ago (using MetaMath).

Sorry if this is obvious in one of the links, but does there exist a high quality “OCR-ed” version of the original text?