Live data from Hacker News

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

Post reply on HN

Print view View original

1–3 of 3 posts

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

#1

Post by gridentio » Wed, Nov 29, 2023, 11:18 AM UTC

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

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

#2

Post by gridentio » Wed, Nov 29, 2023, 11:20 AM UTC

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

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

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

#3

Post by noneoftheabove » Wed, Nov 29, 2023, 12:51 PM UTC

Interesting. What are the competitors for to lean?

Post reply on HN