MIT Computer Scientist Scott Aaronson writes on Nov. 17:
Last Friday, I was at a “Symposium on the Nature of Proof” at UPenn, to give a popular talk about theoretical computer scientists’ expansions of the notion of mathematical proof (to encompass things like probabilistic, interactive, zero-knowledge, and quantum proofs). This really is some of the easiest, best, and most fun material in all of CS theory to popularize. Here are iTunes videos of my talk and the three others in the symposium: I’m video #2, logician Solomon Feferman is #3, attorney David Rudovsky is #4, and mathematician Dennis DeTurck is #5. Also, here are my PowerPoint slides. Thanks very much to Scott Weinstein at Penn for organizing the symposium.This suggests that there are new kinds of proof that have replaced the old style of math proofs. But in fact all the word he described are regular math theorems provable in ZFC like everything else.
Aaronson does describe some other ways of convincing someone that something is true. For example, someone with a complete proof can release info to convince others that he has a proof, without releasing the whole proof or even enough info to recontruct the proof. Some of these ideas have some practical application, such as the holder of a private cryptographic key can convince an authority that he possesses the key, without revealing the key. That evidence might even be called a "proof of possession". But none of these ideas has really changed the notion of a mathematical proof. If you want to get a math paper published in a math journal, you have to supply a proof from axioms just as always.