Verifying Sierpi\'nski and Riesel Numbers in ACL2

TL;DR

This paper presents a method using ACL2 to systematically verify that certain numbers called Sierpinski and Riesel numbers have no primes of specific forms, by checking their covers for non-trivial factors.

Contribution

The paper introduces a formal verification approach in ACL2 for confirming the properties of Sierpinski and Riesel numbers using their covers.

Findings

Successfully verified several Sierpinski and Riesel numbers with ACL2.

Demonstrated the effectiveness of formal methods in number theory verification.

Provided a framework for future automated proofs of similar number classes.

Abstract

A Sierpinski number is an odd positive integer, k, such that no positive integer of the form k * 2^n + 1 is prime. Similar to a Sierpinski number, a Riesel number is an odd positive integer, k, such that no positive integer of the form k * 2^n + 1 is prime. A cover for such a k is a finite list of positive integers such that each integer j of the appropriate form has a factor, d, in the cover, with 1 < d < j. Given a k and its cover, ACL2 is used to systematically verify that each integer of the given form has a non-trivial factor in the cover.