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.
[ Parent
| on HN ]
There are no comments on this comment yet.