Commit 2025-07-31 00:45 2907bf73
View on Github →chore: Clean up typos using OpenAI's GPT-4.1 mini (verified by human) (#27539)
This commit was generated using OpenAI's GPT-4.1 mini and then verified by a human.
A human-written script was run (powered by the aforementioned AI model) on the files № 201-300 in the Mathlib/ folder.