Style lint technical debt

Having done a lot of project maintenance and written a lot of python code, I have many opinions about both. I looked at scripts/lint-style.py and immediately thought of ~5-10 refactoring tasks, from the cosmetic to updating to the contemporary state of defensible python:

• Full mypy strict typing
• Chained if/elif/else -> case/match and assignment operator (:=)
• (unit tests might seem overbearing for tooling, but to use the favorite wording of Claude, there's a high cost of wrong here)
• (pydantic dependency probably also undesirable unless we're willing to require uv for project management of pythonic components, however pydantic would allow for a very easy, defensible, and conventional way to validate input data contracts, for example, style-exceptions.txt. Given how much string scraping lint-style.py is doing, pydantic would be a significant improvement)
• If python code, even as maintenance tooling, we probably would want a pyproject.toml anyway with

  [tool.ruff.lint]
  select = ["E", "W", "F", "I", "N", "UP", "B", "C4", "SIM", "TID", "RUF"]
  

  at a minimum
• Business logic leaking out of python into sidecar shell scripts
• s/argv/argparse/g
• if __name__ == "__main__"

However

A comment near the top of the file says, "This is adapted from the linter for mathlib3. It should be rewritten in Lean," implying at least two constraints on the problems and the strategy of their solutions:

1. What is the project coupling strength to mathlib(4)? Should we work within their conventions, specifically
2. This entire file should be rewritten in lean, basically invalidating or at least dead ending any python improvements?

I'm not very familiar with lean yet, so can't judge the linting usecase or hammer-finding-nails signal. It's usually better for a language's own ecosystem to evaluate and manage style and formatting issues natively. For example: black, isort, pyupgrade, mypy for python, rustfmt, clippy, cargo-audit for rust, gofmt, go vet, goimports for go. Perhaps there's nothing to do here but instrument whatever that is, or contribute to lean tooling directly.

Start by reading scripts/lint-style.py, especially the comment about adapting the mathlib3 linter and rewriting it in Lean. Determine the project's coupling to mathlib and whether Python improvements or Lean tooling are wanted; completion requires an agreed scope and strategy before implementation.