A case stydy about the formalization by pupils of a number theory problem