One of my research goals is the formalization of interesting (to me) theorems from mathematics and computer science. Currently, I am working on a formalization of approximation algorithms to the Set Cover problem. The following table lists some of the formalizations that I, or one of my collaborators, have done in the past.
Project  Author(s)  Availability 

Irrationality of Square Root  R. Gamboa  ACL2 Books 
Exponential Function  R. Gamboa  ACL2 Books 
Trigonometric Functions  R. Gamboa  ACL2 Books 
Fast Fourier Transform  R. Gamboa  ACL2 Books 
Intermediate Value Theorem  R. Gamboa  ACL2 Books 
Maximum and Minimum Theorems  R. Gamboa  ACL2 Books 
Mean Value Theorem  R. Gamboa  ACL2 Books 
Automatic Differentiator  P. Reid R. Gamboa 
ACL2 Books 
Fundamental Theorem of Calculus  M. Kaufmann  ACL2 Books 
Taylor’s Theorem  R. Gamboa B. Middleton 

Inverse Functions  R. Gamboa J. Cowles 
ACL2 Books 
Unique Factorization in Euclidean Domains  J. Cowles R. Gamboa 
ACL2 Books 
Correctness of Hardware Implementation of SQRT  J. Sawada R. Gamboa 

Correctness of a Kalman Filter Implementation  R. Gamboa J. Cowles J. Van Baalen 

CookLevin Theorem  R. Gamboa J. Cowles 

Existence of NonMeasurable Sets  J. Cowles R. Gamboa 
ACL2 Books 
Existence of Transcendental Numbers  R. Gamboa J. Cowles 
ACL2 Books 
Powerlist Data Structure  R. Gamboa  ACL2 Books 
RedBlack Trees  R. Gamboa  DrACuLa Distribution 
Quantum Circuits  L. Helms R. Gamboa 
ACL2 Books 
Medina’s Approximation to Arctangent  R. Gamboa J. Cowles 
ACL2 Books 
Equivalence of Traditional and NonStandard Approach to Calculus  J. Cowles R. Gamboa 
ACL2 Books 
Sierpinski and Riesel Numbers  J. Cowles R. Gamboa 
ACL2 Books 
Vickrey’s Theorem  R. Gamboa J. Cowles 
ACL2 Books 