Reader websites

Three websites where you read a maths paper and click a linked sentence to open the Lean linked to it, beside the text. In Lean Exposition and Proof Reader, the step you are reading is also highlighted on a map of the argument.

Limits: Lean checks the code. Whether a sentence and the code say the same thing is for a person to judge, and I made the links with AI.

Lean Exposition and Quartic Reader show OpenAI’s papers. Proof Reader shows Contextual Embeddings by Frohlich, Foster, Kavvos and Wang, with the authors’ own Lean proof.

Lean is a program that checks mathematical proofs.