News for hackers. Stuff that matters.

A comment on Terence Tao – Machine-Assisted Proofs (February 19, 2025) [video]. Parent comment

Re:Terence Tao – Machine-Assisted Proofs (February 19, 2025)... by newswasboring on Wednesday February 26, 2025 @03:49AM (#43181982)
> I remember seeing this proved before but I can’t be bothered to go look it up again.

I think that is what Lean libraries are for.

[ Parent | on HN ]
Re:Terence Tao – Machine-Assisted Proofs (February 19, 2025)... by sebzim4500 on Wednesday February 26, 2025 @04:33AM (#43182211)
Possibly but lean libraries currently contain a tiny fraction of widely known mathematical results.
[ Parent | on HN ]