3 ms·
Lean4 helped Terence Tao discover a minor error in a recent PFR conjecture paper
- gridentio 3y agoI recently shared another similar mathstodon post https://mathstodon.xyz/@tao/111287749336059662 https://mathstodon.xyz/@tao/111287749336059662 This link, however, is related to a different paper.
- noneoftheabove 3y agoInteresting. What are the competitors for to lean?