[digama]

For what it's worth, here's a proof that the primes are unbounded (and hence infinite) in the proof language Metamath: http://us.metamath.org/mpegif/prmunb.html .

I would classify myself as a "proof programmer" who works with Metamath for much the same reasons as people use Coq (I just happen to prefer Metamath's set theory foundations to type theory). I find the article's claim "Set theory has sufficed as a foundation for more than a century, but it can’t readily be translated into a form that computers can use to check proofs" as outright false for this reason. Mizar is another set theory-based proof system.

If I wanted to prove x <= n -> x = 0 or x = 1 or ... or x = n, I would use http://us.metamath.org/mpegif/leloe.html to turn x <= n <-> x < n or x = n, and http://us.metamath.org/mpegif/zltlem1.html to prove x <= n-1 from x < n. Repeat until you get down to zero to get all n cases.

[sukilot]

What is "all n cases" when you are quantifying over all "n"?. There are an infinitude of cases. You need induction.