Wouldn’t it be nice if every proof was automated by something that shortens the proof and works reliably 100% of the time? This summer, during my internship at Galois, I explored whether one of my favorite tools, SMT solvers, could provide that very solutionAs part of a project aimed at verifying the frontend of the Jolt zkVM, we used an SMT solver to automate Lean proofs, saving over 6,800 lines of Lean code that would have been otherwise written by hand. Our results point towards the possibili...