Commit 2025-07-31 02:52 192b251a
View on Github →chore: fix many typos (powered by OpenAI's GPT-4.1 mini) (#27545) Co-authored by @Rob23oba. Powered by OpenAI's GPT-4.1 mini. @Rob23oba wrote a Lean program to find all tokens used in Mathlib's declarations, and posted a full list. Then, I ran OpenAI's aforementioned model on said list, and got a list of about 300 potential typos. Then I replaced them manually using VSCode's editor and used the deprecation script. Since this is done using a frequency analysis algorithm, naturally it will miss "contextual typos", where the typo is still a valid word but used in the wrong context.