News for hackers. Stuff that matters.

A comment on Problems of Traditional Math Notation (2004). Parent comment

Re:Problems of Traditional Math Notation (2004) by adamnemecek on Monday November 06, 2017 @02:21AM (#15633893)
More like coq
[ Parent | on HN ]
Re:Problems of Traditional Math Notation (2004) by gnulinux on Monday November 06, 2017 @10:42AM (#15636212)
Coq is intuitionistic, classical proofs cannot be expressed. Mathematicians almost always (unless intuitionistic math is your niche) use classical proofs.
[ Parent | on HN ]
Re:Problems of Traditional Math Notation (2004) by adamnemecek on Monday November 06, 2017 @11:41AM (#15636658)
It kinda is yes. I don’t understand why classical proofs are still a thing.
[ Parent | on HN ]