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 solution
