This blog continues the Calculemus series, where we'll propose a new proof exercise daily and publish the solutions using Lean4 and Isabelle/HOL.