This is a implementation of a counter example to the unit conjecture for group rings "https://www.gilesgardam.com/papers/unit-conjecture-counterexamplev3.pdf" in Lean. You can find the statement at the end of Theorem1. 
The file Theorem1 follows the notation of the paper of Giles Gardam. 
In order to compile you might have to make sure that you have enough memory accessible (~6GB) and it might take several minutes.