[auggierose]

How proofs work is really simple. The question is, how do you work inside a proof assistant, which kind of math is easy to express, and what is difficult? If you leave that to the CS people, math will become computer science. The ultimate logician was Gödel, and he clearly was a mathematician.

[runeblaze]

> How proofs work is really simple

idgi. If you do your 101 logic class often you learn natural deduction, and how do you formalize natural deduction in a computer system? (Hint: type theory is "natural" for this).

Also how proofs work is far from simple.

[auggierose]

How proofs work is pretty simple, and you don't need types to do natural deduction. As usual, types only complicate the picture. Here is a more straightforward and natural way to treat natural deduction: http://abstractionlogic.com .

[runeblaze]

sure of course one does not need types to do natural deduction… if you throw what you showed me to your average maths undergrad in the US they will get confused — I truly don’t see how proofs are simple

[auggierose]

It is a matter of presentation and what people are used to. In particular, in abstraction logic, in the simplest (and most general!) case, you only have these proof rules: Axiom, Assume, AddAnte, BindAnte, FreeAnte, InferAnte. If we just focus on this case, we can choose simpler names for these rules: Axiom, Assume, Add, Bind, Free, Infer. That's it. That is all there is to proof.

[kthielen]

What do you have to say about Curry-Howard?

[auggierose]

Most overrated isomorphism in the history of machine-assisted proof.