LARA Labs 03 Isabelle presented by Steven Obua. You may also wish to check the video of Steven's talk about mechanizing the Proof of Kepler's Conjecture.
