*The only axiom I cannot avoid is propositional extensionality (which is kind of unavoidable in any non-toy proof in Lean).
There's a common trope of internet comments where you see people say they went off and did their own thing from first principles, pointedly avoiding existing work and preferring to follow their own ideas. And then you look at the thing and it's nigh invariably the disconnected ramblings of a person convinced of their own misunderstood genius.
But if the computer vouches for you, hard to avoid taking it seriously, that's the highest standard of rigor we have :)
(Nice proof by the way!)
Please do! This looks like the perfect size and complexity to learn the basics, I'd love a structured walk-through of the code.
Myself, I am not a constructivist in any way. I just like to produce data whenever I can, and I believe that sometimes constructive proofs give additional insights for the objects we study; therein lies my interest in constructive arguments.
I think the answer is "Lean is constructive if you use the base system without known non-constructive axioms".
Constructive proofs also have an interesting relationship with algorithms to construct the object in question. (Funny enough, to proof some algorithms correct, you can use non-constructive proofs.)
For example, Euclid's classic proof (the one that goes 'multiply all the primes you know, add 1') is at least implicitly constructive, because you can factor that new number with a well-known algorithm to get at least one new prime.
Infinity is quite a bit bigger than 1.
Given primes p1, p2, …, pn, multiply them, add 1, and factor the result. All its prime factors are new primes.
For example, given {5,7,11}, the product is 385. Adding one yields 386.
Factoring that learns you that 386 = 2 × 193. Both are primes not in the original list.
If you start with {}, the series you get is
{} ⇒ 2 = 2
{2} ⇒ 3 = 3
{2,3} ⇒ 7 = 7
{2,3,7} ⇒ 43 = 43
{2,3,7,43} ⇒ 1807 = 13 × 139
{2,3,7,43,13,139} ⇒ 3263443 = 3263443
(I wonder whether you need to be able to factor efficiently to get your hands on that list, or whether there's some way around that.)