Paulson is a lead developer of Isabelle , a proof assistant that is not based on dependent types.
> Is this the mathematician's variant of "my language is better than your language",
Almost. A closer analogy is comparing paradigms, say OOP vs functional programming.
Isabelle is different from the big three - rocq. lean and agda. The latter three have propositions as types. The type of your function is the theorem statement. The function body is the proof.
Isabelle works differently.
Author makes a convoluted argument that (a) one doesn't have to stick to the currently popular paradigm and (b) in conjunction with AI, Isabelle offers distinct benefits.
I think the author is confkating two different things.
There are technical problems with sticking to constructive purity when it comes to mathematics (setoid hell, avoiding excluded middle, real number formalization etc).
Then there are social aspects. The community's 'cultist' ( his words) adherence to constructive logic. Saying this is the reason rocq lost out to lean seems wrong.
Firstly, there is value of the attempt. By staying true to constructive logic, there was a lot of progress (compcert verified c compiler, cubical agda etc).
Secondly, there were other confounding variables (tooling, network effects). Claiming rocq lost out to lean due to community's obsession is a bit of reductive argument.
But author is an expert. I will defer to him.
His point about sledgehammer approach working well in the new AI world is very interesting though.
> Is this the mathematician's variant of "my language is better than your language",
Almost. A closer analogy is comparing paradigms, say OOP vs functional programming.
Isabelle is different from the big three - rocq. lean and agda. The latter three have propositions as types. The type of your function is the theorem statement. The function body is the proof. Isabelle works differently. Author makes a convoluted argument that (a) one doesn't have to stick to the currently popular paradigm and (b) in conjunction with AI, Isabelle offers distinct benefits.