@xenaproject @ProfKinyon I also enjoyed working through "Theorem Proving in Lean4" and look forward to checking out "Mathematics in Lean".