FLT is a negative statement ("there are no nonzero integers x, y, z such that..."), and proofs by contradiction are constructively valid for proving negative statements.
For what it's worth, I don't think that Kevin Buzzard is the person you should talk to if you are interested in proof assistant design. As far as I know, Buzzard does not consider himself to be an expert in type theory or in proof assistants, and claims to be a mere user.
AFAICT, this issue only comes up if you form the quotient of a proposition by a relation. But there is no point in doing that (all the proofs of a proposition are already equal!) so it's not an issue in practice and it wouldn't be difficult to fix.
However, Lean's SR is broken in other ways which do show up in practice: definitional proof irrelevance is incompatible with Lean's computation rule for Acc. That one is much harder to fix.
Computation is the difference. In Lean, applying the universal property of the quotient (`Quotient.lift f Hf`) to an element that is of the form `Quotient.mk a` reduces to `f a`.
This rule is fine in itself, but the Lean developers were not sufficiently careful and allowed it to apply for quotients of propositions, where it interferes with the computation rules for proof irrelevance and ends up breaking subject reduction (SR is deeply linked to computation when you have dependent types!) [0]. It is not really a problem in practice though, since there is no point in quotienting a proposition.
There is a nice illustration of a 2-sphere wrapped twice around another 2-sphere on the Wikipedia article for the homotopy groups of spheres [0].
Now, there are many ways of proving that there is only one way (up to homotopy) of wrapping a 2-sphere n times around another 2-sphere, but all of them are fairly involved. The simplest proof comes from an analysis of the Hopf fibration, which roughly describes a relation between the 1-sphere, the 2-sphere and the 3-sphere [1]. Other than this, it follows from the theory of degrees for continuous mappings, or from the Freudenthal suspension theorem and some basic homological computations.
This makes me wonder whether the usual order for function application is an artifact of the S-V-O sentence structure in western European languages. Maybe if Euler had been raised in a language with a S-O-V sentence structure, we would write (x)f instead.
Plus, reverse function application/composition works better with our tendency to write the domain of the function before its range. Given f : A -> B and g : B -> C, the composite function is written as g o f which is mildly annoying.
That's pretty cool, but the downsides of switching to RRA are not only about user experience. When the result is 0.0000000..., the calculator cannot decide whether it's fine to compute the inverse of that number.
For instance, 1/(atan(1/5)-atan(1/239)-pi/4) outputs "Can't calculate".
Well alright, this is a division by zero. But then you can try 1/(atan(1/5)-atan(1/239)-pi/4+10^(-100000)), and the output is still "Can't calculate" even though it should really be 10^100000.
ZFC is way worse than Presburger arithmetic -- since it is undecidable, we know that the length of the minimal proof of a statement cannot be bounded by a computable function of the length of the statement.
This has little to do with the usefulness of LLMs for research-level mathematics though. I do not think that anyone is hoping to get a decision procedure out of it, but rather something that would imitate human reasoning, which is heavily based on analogies ("we want to solve this problem, which shares some similarities with that other solved problem, can we apply the same proof strategy? if not, can we generalise the strategy so that it becomes applicable?").
There's a bit of a definition issue at play here. When Andreas Blass and Noah Schweber say that there is no proof system for PA_2, they mean that there is no effective proof system that is complete for the full semantics. If you subscribe to their definition of a proof system, you end up saying that there is no such thing as a proof in PA_2, and thus that incompleteness is meaningless -- which I personally find a bit silly.
On the other hand, proof theorists and computer scientists are perfectly happy to use proof systems for second order logic which are not complete. In that case, there are many effective proof systems, and given that the axioms of PA_2 are recursively enumerable (they are in finite number!), Gödel's incompleteness will apply.
If you are still not convinced, I encourage you to decide on a formal definition of what you call PA_2, and what you call a proof in that system. If your proof system is effective, and your axioms are recursively enumerable, then the incompleteness theorem will apply.
If you look at the Wikipedia page for second order arithmetic, there is a definition in the language of first order logic as a two-sorted theory comprising a handful of basic axioms, the comprehension scheme, and the second-order induction axiom (in your first mathoverflow link, this is called Z_2):
An other equivalent option would be to use the language of second order logic, where you only need a finite amount of axioms, because the comprehension scheme is already included in the rules of second order logic. This one is PA_2.
Since these definitions do not refer to anything uncomputable such as mathematical truth, both systems are clearly recursively enumerable. This means that Gödel's incompleteness theorem applies to both, in the sense that you can define a sentence in the language of arithmetic that is unprovable in Z_2 or PA_2, and whose negation is also unprovable.
All of these considerations have little to do with models or categoricity, which are semantic notions. I think your confusion stems from the fact that model theorists have the habit of using a different kind of semantics for Z_2 (Henkin semantics) and PA_2 (full semantics). Henkin semantics are just first order semantics with two sorts, which means that Gödel's completeness theorem applies and there are nonstandard models. Full semantics, on the other hand, are categorical (there is only one model), but this has nothing to do with the axioms not being recursively enumerable -- it is just because we use a different notion of model.
PS: I certainly do not consider mathematics to be included in computer science. Even though as a logician, I have been employed in both mathematics departments and computer science departments...
The axioms of second order Peano arithmetic are certainly recursively enumerable, in fact you can pick a formulation that only uses a finite number of axioms. And second order arithmetic is much weaker than the type system of Lean, which is probably somewhere between Zermelo set theory and ZFC set theory in terms of proof-theoretic strength.
More generally, I think that computer scientists (in particular PL theorists and type theorists) are much more likely to use powerful logics than mathematicians, with the obvious exception of set theorists.
