Since the proof of the four color theorem in 1976, computer-generated proofs have become a reality in mathematics and computer science. During the last decade, we have seen formal proofs using verified proof assistants being used to verify the validity of such proofs.
Outside the world of formal proofs, computer-generated proofs are flourishing, too, and growing to tremendous sizes. The proof of Erd " o s' discrepancy conjecture for @math from 2014 @cite_10 has been touted as one of the largest mathematical proofs and produced approx. 13 GB of proof witnesses. Such large-scale proofs are extremely challenging for formal verification. Given the current state of theorem provers and computing equipment, it is unthinkable to use 's approach @cite_3 of importing an based on the proof witnesses into Coq, a process clearly prohibitive for such large-scale proofs as we consider.
@cite_10 @cite_3
2964092005 205472424
In 1930s Paul Erdős conjectured that for any positive integer C in any infinite ±1 sequence (x n ) there exists a subsequence x d , x 2d , x 3d ,…, x kd , for some positive integers k and d, such that ( i=1 ^k x_ id >C ). The conjecture has been referred to as one of the major open problems in combinatorial number theory and discrepancy theory. For the particular case of C = 1 a human proof of the conjecture exists; for C = 2 a bespoke computer program had generated sequences of length 1124 of discrepancy 2, but the status of the conjecture remained open even for such a small bound. We show that by encoding the problem into Boolean satisfiability and applying the state of the art SAT solver, one can obtain a discrepancy 2 sequence of length 1160 and a proof of the Erdős discrepancy conjecture for C = 2, claiming that no discrepancy 2 sequence of length 1161, or more, exists. We also present our partial results for the case of C = 3. Proof-by-reflection is a well-established technique that employs decision procedures to reduce the size of proof-terms. Currently, decision procedures can be written either in Type Theory--in a purely functional way that also ensures termination-- or in an effectful programming language, where they are used as oracles for the certified checker. The first option offers strong correctness guarantees, while the second one permits more efficient implementations. We propose a novel technique for proof-by-reflection that marries, in Type Theory, an effectful language with (partial) proofs of correctness. The key to our approach is to use simulable monads, where a monad is simulable if, for all terminating reduction sequences in its equivalent effectful computational model, there exists a witness from which the same reduction may be simulated a posteriori by the monad. We encode several examples using simulable monads and demonstrate the advantages of the technique over previous approaches.