2 ms·
Coq is intuitionistic, classical proofs cannot be expressed. Mathematicians almost always (unless intuitionistic math is your niche) use classical proofs.
by gnulinux 9y ago
Coq is intuitionistic, classical proofs cannot be expressed. Mathematicians almost always (unless intuitionistic math is your niche) use classical proofs.
- adamnemecek 9y agoIt kinda is yes. I don’t understand why classical proofs are still a thing.