This blog continues the Calculemus series, where we propose a new proof exercise every week and publish the solutions using Lean 4.