Lean4 helped Terence Tao discover a minor error in a recent PFR conjecture paper

I recently shared another similar mathstodon post https://mathstodon.xyz/@tao/111287749336059662

This link, however, is related to a different paper.

Interesting. What are the competitors for to lean?