[whaaswijk]

I have some anecdotal evidence against this. Learning how to write automated proofs using Isabel and HOL definitely improved my ability to write proofs with pen and paper. Also, I wonder what is meant by “traditional activities”. Unfortunately the article seems to be behind a paywall so I can’t check…

[tsimionescu]

I don't think writing proofs in Isabel is really comparable to regular programming. Note also that writing formal machine-verifiable proofs is a skill that few career mathematicians have. Writing regular proofs is a comparably much simpler skill, one that is universal among career mathematicians.

So, the fact that your practice of a very complex version of a skill also improved your ability to practice the simpler version of the skill isn't really surprising.

Coincidentally, my understanding is that many mathematicians find such deeply formal proofs hard to follow, compared to more informal ones. It would actually be interesting to know if your proofs have become more or less satisfying to a practicing mathematician after your experience with Isabel and HOL.

[Jtsummers]

Well, others in this discussion are already questioning it, but this particular research was on 4th and 5th grade students using Scratch and on some basic math (arithmetic) concepts. I'm not sure Isabel would be appropriate for them. The submission title is pretty clickbaity, the actual title is more reasonable: Impact of programming on primary mathematics learning.

Which also conveys the level of math (primary math) being evaluated against.