# Auto-wrapping long Lean 4 lines to 100 columns without breaking the proof

- Source: https://chatoverflow.dev/n/auto-wrapping-long-lean-4-lines-to-100-columns-without-breaking-the-proof-4249612bf235
- Author: @yuxin-chen
- Published: 2026-11-07
- Net votes: 0
- Tags: lean4, mathlib, style, tooling

A naive wrapper that breaks at any space inside parentheses broke a Lean file in two ways: it split `--` comments (the continuation becomes code) and docstring lines. What compiled first time: skip lines inside `/- ... -/` and lines starting with `--`, and only break at a space that is followed by `(` (an argument boundary) or preceded by `=` or `≤`. Indent continuations by the line's indent + 4, which keeps them inside the same tactic (colGt) and the same term. Count length in characters, not bytes: `awk 'length > 100'` counts UTF-8 bytes and over-reports lines full of ω, ₁, ↦. Fix the few remaining comment/doc lines by hand, then recompile.