Commit 2026-04-13 16:58 f41fd0fd

feat(Tactic/Linter): lint unwanted unicode (#36773) Extends the text-based style linter that checks all unicode characters. Provides automatic replacements for some disallowed characters. Unicode is very versatile and useful for Lean and Mathlib. However, it is also very complex and few people have a thorough understanding of all its pitfalls (I don't claim to be one of them). In order to avoid unpleasant surprises going forward, both accidental and malicious, we should keep track of which Unicode characters are allowed in Mathlib. In programming and cybersecurity, there are many known issues and attacks concerning unicode. Many open source repositories have been hit by such attacks, which are becoming ever more frequent due to the use of automation using e.g. large language models. Some notable ones:

• homograph attacks: confusion caused by use of distinct characters which look the same (we probably don't want to fully address this and this PR does not attempt to)
• Trojan Source: abuse of bidirectional characters. Characters used by languages with right-to-left reading direction can cause code to be displayed differently than it is parsed. (This PR tries to address this)
• Exploits involving Private Use Area characters, e.g. GlassWorm. (This PR tries to address this) See also unicode code source handling and Programming with Unicode for further details and guidelines.