News for hackers. Stuff that matters.

A comment on Lean4 helped Terence Tao discover a small bug in his recent paper. Parent comment

Re:Lean4 helped Terence Tao discover a small bug in his rece... by firedaemon on Saturday October 28, 2023 @04:52PM (#38053254)
I have always used it to mean “solves problems 10x faster” not “produces 10x code”.

The latter would be a bad thing.

[ Parent | on HN ]

There are no comments on this comment yet.