AI is a tool, like any other. Imagine you invented a new machine gun that fires faster and has less recoil but james more often. Who will be able to put the new machine gun to better use -- new recruits or veteran soldiers? C'mon.
That might be a trick question I think. As a veteran I would drop one enemy, take their AK-47 and drop my M-16 and start collecting ammo for my nifty old but reliable AK-47 that does not jam when it gets a little dirty.
I mean documentation can be wrong whereas types can't, so it seems like it's strictly a worse tool if your goal is to understand what's actually going on and not what someone said was going on at some point in the past.
types can be (and almost always are) overly restrictive, preventing otherwise valid code from running. they can also be under powered, and not expressing necessary invariants for the algorithm.
I didn't make any claims about that, just that they can't be wrong. And by that, I didn't mean you can't choose the wrong types, just that once you've chosen types that compile they can't be incompatible or other than what they are.
That being said, I've always found the argument that types can be overly restrictive and prevent otherwise valid code from running unconvincing. I've yet to see dynamic code that benefits from this alleged advantage.
Nearly universally the properly typed code for the same thing is better, more reliable and easier for new people to understand and modify. So sure, you can avoid all of this if the types are really what bother you, but it feels a bit like saying "there are stunts I can pull off if I'm not wearing a seatbelt that I just can't physically manage if I am."
If doing stunts is your thing, knock yourself out, but I'd rather wear a seatbelt and be more confident I'm going to get to my destination in one piece.
I am assuming you mean it's a bigger concern in Lean than other languages because of what people are attempting to do with it (formalize all of math)? Because the language itself, somewhat by design and somewhat by nature, seems to be more future proof than any other language I've ever used.
I'm not an expert but I'd say based on my experience with Lean so far, the answer is yes. eg. I have entered some proofs from the Lean guide and then replaced tactics with `apply?` which searches for tactics to meet the goal, and eg. reduced this example from the guide:
theorem and_commutative (p q : Prop) : p ∧ q → q ∧ p :=
fun hpq : p ∧ q =>
have hp : p := And.left hpq
have hq : q := And.right hpq
show q ∧ p from And.intro hq hp
To this:
theorem and_commutative' (p q : Prop) : p ∧ q → q ∧ p := by
exact fun a ↦ id (And.symm a)
Presumably the same thing could be done for each part of a more complicated proof and could be done so at each step automatically.
Do you explicitly tell it that it's writing production code? I find giving it appropriate context prevents or at least improves behaviors like this.