The compiled proof does take a few hours to finish verifying on a typical laptop. But obviously the many experiments and enumerations along the way took much more total processing power.