News for hackers. Stuff that matters.
Re:Doing a math assignment with the Lean theorem prover by dhosek on Tuesday April 07, 2020 @11:46AM (#22804267)
Aesthetically, two-column proofs are miserable, but they have the advantage that the logic is very clearly laid out. There's no chance to hand-wave when every step of the proof needs to be explicitly justified.

There are no comments on this comment yet.