I’m currently engaged in a variety of different research projects.
John Cowles and I have been using ACL2(r) to prove that various series converge or diverge. For instance, the sum of the reciprocals of the primes diverges, while the sum of the reciprocals of the squares converges. This can be interpreted to mean that primes are much more common that squares! John and I continue to explore questions of this type.
At the suggestion of David Russinoff, the two of us are also verifying various algorithms related to the transcendental instructions in the x86 instruction set. These are particularly interesting to me, because these theorems cannot be stated in ACL2, since they depend heavily on the entire real number line. So this is a perfect application of ACL2(r). David suggested this project when he was working at AMD, and he continues to encourage us from Intel.
Speaking of Intel, a few years ago, John and I proved the existence of transcendental numbers in ACL2(r), following Cantor’s famous proof. We have been meaning to prove the existence of a specific transcendental number, but that project was in the back burner, until Sandip Ray of Intel asked about a proof that powers of \(e\) are transcendental. What he wants is a proof of Lindenmann’s theorem, which is that \(e^\alpha\) is transcendental for any non-zero algebraic number \(\alpha\). Why would Intel be interested in this result? It turns out that it is very practical, because it relates to the security of some cryptographic algorithms based on transcendental numbers. That is all they are willing to share.
At the ACL2 Workshop in Vienna this year, Anna Slobodova and Warren Hunt suggested to John Cowles and me that ACL2(r) may be able to reason about analog circuits. Anna presented an invited talk at ITP describing the verification pipeline in use at Centaur Technology. Engineers at Centaur are able to reason about their digital circuits during the design process. This is incredible, given that the verification efforts are happening at the same time as design changes are taking place! Unfortunately, they do not have a similar verification pipeline for analog circuits. It is possible that ACL2(r) can help, and John and I have started exploring this. At least one of us will visit Anna and Warren in Austin this November, and we’ll see if there is something here that is worth pursuing.