what makes proof 'real'?

[Kayli]

I was playing with coq one day ... and stumbled on its tactics language. It was really hard to grasp and I was pleasantly surprised to hear the same from tsoding in one of his videos ... but he keeps saying that coq provides 'real proofs' and somehow noq proofs can't be considered 'real'. Can someone explain me what is the difference? What noq is missing for it proofs to be considered 'real'? Any help is appreciated!

[casey2069]

In short, a noq proof can convince most humans, but it can't convince coq. coq itself is based on CoC  which is a foundation for mathematics. So any proof in coq is equivalent to a proof using CoC.  Meanwhile, noq is just "pencil and paper on steroids." if I say sum_id :: 0 + A = A it's left to the mathematician to decide what each symbol refers to, and explain to the reader via comment, noq doesn't know or care.

Another interpretation of "real proof" is that coq proofs are constructive while noq proofs need not be, but I doubt he meant that.

Back to the question, a "coq proof" implies the existence of a (real) proof that is valid in a certain mathematical foundation (CoC), while a "noq proof" does not necessarily imply the existence of a proof in any mathematical foundation. 

[Kayli]

Thanks Casey, this helps a bit. Are you trying to say that before Thierry Coquand invented CoC, mathematical proofs somehow were 'less real'? What I'm trying to do here, is to strip all institualization fuss from definition of what constitutes a 'real proof' that can be taken seriously ... let's say, in a scientific paper.

Don't get me wrong, but its just hurts to see that proof of 3+4=7 needs some mysterious CoC thing which is "at the top of Barendregt's lambda cube" as wikipedia states. I'm 38yo software engineer with 17 years of practical experience and somehow some basic stuff like this slips away from me any time I'm trying to read about it. Im starting to think that one of the roles of modern educational institutions is to make common knowledge as cryptic as it is possible ... its a kind of mathematical priesthood that creates those mazes in order to justify their own existence. I really hope that I'm wrong, but please, can you explain why do we need something more than noq to prove that 3+4=7 ?

Ideally, such proofs should be accessible to kids in high school ... I really struggling to get why things need to be so overcomplicated.

Why axioms + transformation rules for symbols are still not good enough? and how come noq proofs that tsoding illustrates are not constructive?

[casey2069]

No, there is nothing less real about proofs before CoC. The major use case of coq is to verify programs (coq assisted proofs) that are too long to read, against a known standard (CoC). In the same way that C code before ANSI C is real. For writing most papers, coq is a completely unnecessary hindrance. But this is open to interpretation, some mathematicians (at least 1) have coq verify every proof they publish. Some list out each axiom and theorem in great detail, refer to each when used. Most try to be brief and trust their target audience to fill in the gaps.

A proof being constructive was a red herring on my part. I can't recall tsoding illustrating any nonconstructive proofs, but I'll use an example of a nonconstructive proof and show why noq allows such arguments and possibly why he doesn't consider noq proofs as "real".

# Theorem: An irrational raised to another irrational can be rational.
# Fact 1: sqrt(2) is irrational.
# Fact* 2: sqrt(2)^sqrt(2) is either rational or irrational. 
# If it's rational, our theorem is proved. If not, consider (sqrt(2)^sqrt(2))^sqrt(2).
load "../std/std.noq"
exp_assoc       :: (A^B)^C = A^(B\*C)
sqrt_def        :: (sqrt(A)^2) = A
var         :: sqrt(2)     = x
simplify        :: (x^x)^x {
exp_assoc                       | 0
square                      |!0
var                 |!all
sqrt_def                | all
sqrt_def                | all
}
# Returns 2, a rational number, and our theorem is true. 
# This is non-contructive as we have not shown that sqrt(2)^sqrt(2) is irrational.
# *Constructive logic leaves out the law of exluded middle. 

In my opinion, the proof is not complete (i.e not a real proof) without the first 5 comments, and that is arguably not part of noq. In contrast, there is no argument against a coq proof, aside from bugs in how coq implements CoC.

[Kayli]

Oh, I see, you mean that coq provides a formal way to express a theorem about irrational numbers using its own language. But if we try to apply same reasoning to 3+4=7 proof, what do you think is missing in noq to make such proof 'real'?

[rexim]

Nothing actionable here