Proofs as Games

Quite interesting, but technical,  a unique view of proofs.  Below the intro.

Technical Perspective: On Proofs, Entanglement, and Games

By Dorit Aharonov, Michael Chapman

Communications of the ACM, November 2021, Vol. 64 No. 11, Page 130  10.1145/3485596

What is a proof? Philosophers and mathematicians have pondered this question for centuries. Theoretical computer science offers a rigorous handle on this deep question. One can think of a proof as a two-player game: an all-powerful though un-trusted prover who provides a proof of the statement, and a computationally weak verifier who needs only to verify it. In fact, NP problems can be presented exactly in this verifier-prover language. Viewing proofs as games turned out to be remarkably fruitful.

 For example, interactive proofs were invented, resembling Socratic dialogues; these are games in which the prover and verifier exchange (possibly randomized) messages. And, why just one prover? In multi-prover interactive proofs (MIP) several non-communicating provers are involved. This gave birth to beautiful concepts such as zero knowledge and probabilistically checkable proofs (PCPs) with immense impact not only theoretically but also in practice, for example, in digital currency.

The following paper studies quantum interactive proofs. Here the provers are allowed to share an entangled quantum state; this resembles sharing a random bit string, except quantum states have those funny, stronger-than-classical correlations; a prototypical example is the Einstein-Podolsky-Rosen (EPR) state, which was said by Einstein to allow "spooky action at a distance." Can quantum correlations be used to prove stronger statements?   ... ' 

Hacker Resistant Cloud Software

From a former employer of mine.   Don't understand the details as yet.  See that it is to be presented shortly.   A proof?  See also the paper mentioned below for additional details. 

Columbia Team Builds Hacker-Resistant Cloud Software System   By Columbia University

Columbia University researchers have developed a system that guarantees — through a mathematical proof — the security of virtual machines in the cloud.

They discuss the system in "A Secure and Formally Verified Linux KVM Hypervisor,"   to be presented at the 42nd IEEE Symposium on Security & Privacy on Wednesday (May 26).

"This is the first time that a real-world multiprocessor software system has been shown to be mathematically correct and secure," says Jason Nieh, professor of computer science at Columbia. "This means that users' data are correctly managed by software running in the cloud and are safe from security bugs and hackers."

The work is the first to verify the widely-used KVM hypervisor, which is used to run virtual machines by cloud providers. "We've shown that our system can protect and secure private data and computing uploaded to the cloud with mathematical guarantees," says Xupeng Li, a Ph.D. student and co-lead author of the paper.

From Columbia University 

Automated Math Reasoning

In our earliest AI courses,we learned about theorem proving using AI. And yes, it was not automated math reasoning.  But it gave you the hope that it could be done, if only you could state the problem at hand as purely mathematical.   Or even parts of it.  But it was never so.  Like the article says, it rarely intersects exactly with the real world, except for elements of the real world that are also approximations within contexts.  Bottom line, its still hard.    Good article explains it, with hopes for the next generation.

How Close Are Computers to Automating Mathematical Reasoning? in Quanta Mag.  Stephen Ornes
Contributing Writer 

AI tools are shaping next-generation theorem provers, and with them the relationship between math and machine.

n the 1970s, the late mathematician Paul Cohen, the only person to ever win a Fields Medal for work in mathematical logic, reportedly made a sweeping prediction that continues to excite and irritate mathematicians — that “at some unspecified future time, mathematicians would be replaced by computers.” Cohen, legendary for his daring methods in set theory, predicted that all of mathematics could be automated, including the writing of proofs.

A proof is a step-by-step logical argument that verifies the truth of a conjecture, or a mathematical proposition. (Once it’s proved, a conjecture becomes a theorem.) It both establishes the validity of a statement and explains why it’s true. A proof is strange, though. It’s abstract and untethered to material experience. “They’re this crazy contact between an imaginary, nonphysical world and biologically evolved creatures,” said the cognitive scientist Simon DeDeo of Carnegie Mellon University, who studies mathematical certainty by analyzing the structure of proofs. “We did not evolve to do this.”

Computers are useful for big calculations, but proofs require something different. Conjectures arise from inductive reasoning — a kind of intuition about an interesting problem — and proofs generally follow deductive, step-by-step logic. They often require complicated creative thinking as well as the more laborious work of filling in the gaps, and machines can’t achieve this combination.

Computerized theorem provers can be broken down into two categories. Automated theorem provers, or ATPs, typically use brute-force methods to crunch through big calculations. Interactive theorem provers, or ITPs, act as proof assistants that can verify the accuracy of an argument and check existing proofs for errors. But these two strategies, even when combined (as is the case with newer theorem provers), don’t add up to automated reasoning.  .... "

Provability and Machine Learning

Interesting point,  but the point being made is rarely useful in practical mathematics.   Just because something cannot be rigorously proved does not mean it is not practically useful.    Results that are used in AI methods are statistical, not exact logic.   Still what is shown does claim to link the related limitations of logic and machine learning.  Now how does that limit ML in practice?

Unprovability comes to machine learning  in Nature

Scenarios have been discovered in which it is impossible to prove whether or not a machine-learning algorithm could solve a particular problem. This finding might have implications for both established and future learning algorithms.

During the twentieth century, discoveries in mathematical logic revolutionized our understanding of the very foundations of mathematics. In 1931, the logician Kurt Gödel showed that, in any system of axioms that is expressive enough to model arithmetic, some true statements will be unprovable 1. And in the following decades, it was demonstrated that the continuum hypothesis — which states that no set of distinct objects has a size larger than that of the integers but smaller than that of the real numbers — can be neither proved nor refuted using the standard axioms of mathematics2–4. Writing in Nature Machine Intelligence, Ben-David et al.5 show that the field of machine learning, although seemingly distant from mathematical logic, shares this limitation. They identify a machine-learning problem whose fate depends on the continuum hypothesis, leaving its resolution forever beyond reach. ..... " 

Paper: https://www.nature.com/articles/s42256-018-0002-3