Related papers: Proof Verification Can Be Hard!
A proof is one of the most important concepts of mathematics. However, there is a striking difference between how a proof is defined in theory and how it is used in practice. This puts the unique status of mathematics as exact science into…
How does the mathematical community accept that a given proof is correct? Is objective verification based on explicit axioms feasible, or must the reviewer's experiences and prejudices necessarily come into play? Can automated provers avoid…
Practicing mathematicians often assume that mathematical claims, when they are true, have good reasons to be true. Such a state of affairs is "unreasonable", in Wigner's sense, because basic results in computational complexity suggest that…
Despite significant developments in Proof Theory, surprisingly little attention has been devoted to the concept of proof verifier. In particular, the mathematical community may be interested in studying different types of proof verifiers…
With the relentless rise of computer power, there is a widespread expectation that computers can solve the most pressing problems of science, and even more besides. We explore the limits of computational modelling and conclude that, in the…
This is a survey on propositional proof complexity aimed at introducing the basics of the field with a particular focus on a method known as feasible interpolation. This method is used to construct "hard theorems" for several proof systems…
In considering the reliability of numerical programs, it is normal to "limit our study to the semantics dealing with numerical precision" (Martel, 2005). On the other hand, there is a great deal of work on the reliability of programs that…
Proof scores can be regarded as outlines of the formal verification of system properties. They have been historically used by the OBJ family of specification languages. The main advantage of proof scores is that they follow the same syntax…
This paper explores the relationship of artificial intelligence to the task of resolving open questions in mathematics. We first present an updated version of a traditional argument that limitative results from computability and complexity…
We extend the theoretical framework of proof mining by establishing general logical metatheorems that allow for the extraction of the computational content of theorems with prima facie "non-computational" proofs from probability theory,…
Artificial intelligence assisted mathematical proof has become a highly focused area nowadays. One key problem in this field is to generate formal mathematical proofs from natural language proofs. Due to historical reasons, the formal proof…
If no optimal propositional proof system exists, we (and independently Pudl\'ak) prove that ruling out length $t$ proofs of any unprovable sentence is hard. This mapping from unprovable to hard-to-prove sentences powerfully translates facts…
Real-life conjectures do not come with instructions saying whether they they should be proven or, instead, refuted. Yet, as we now know, in either case the final argument produced had better be not just convincing but actually verifiable in…
Verifying software correctness has always been an important and complicated task. Recently, formal proofs of critical properties of algorithms and even implementations are becoming practical. Currently, the most powerful automated proof…
The proofs first generated by automated theorem provers are far from optimal by any measure of simplicity. In this paper I describe a technique for simplifying automated proofs. Hopefully this discussion will stimulate interest in the…
Quantum advantage is notoriously hard to find and even harder to prove. For example the class of functions computable with classical physics actually exactly coincides with the class computable quantum-mechanically. It is strongly believed,…
General acceptance of a mathematical proposition $P$ as a theorem requires convincing evidence that a proof of $P$ exists. But what constitutes "convincing evidence?" I will argue that, given the types of evidence that are currently…
In logic there is a clear concept of what constitutes a proof and what not. A proof is essentially defined as a finite sequence of formulae which are either axioms or derived by proof rules from formulae earlier in the sequence.…
Though the truths of logic and pure mathematics are objective and independent of any contingent facts or laws of nature, our knowledge of these truths depends entirely on our knowledge of the laws of physics. Recent progress in the quantum…
The reflection principle is the statement that if a sentence is provable then it is true. Reflection principles have been studied for first-order theories, but they also play an important role in propositional proof complexity. In this…