ABSTRACT. Benchmarking automated theorem proving (ATP) systems using standardized problem sets is a well- established method for measuring their performance. However, the availability of such libraries for non-classical logics is very limited. In this work we seek to start a discussion of benchmarks for Girard’s linear logic and some of its variants. For some quick bootstrapping of the collection of problems, we use translations of the collection of Kleene’s intuitionistic theorems in the traditional monograph Introduction to Metamathematics. We analyze four different translations of intuitionistic logic into linear logic and compare their proofs using linear logic based provers with focusing.