Below are the specific technical rebuttals to J.D. Boyd's article:

>On alleged intrinsic contradictions (FA1)
“There is no contradiction in the set-up of the log-theta-lattice of IUT.” Claims that Lean is “fundamentally incapable” of checking this are “entirely inconceivable,” and the idea that validity is “subjective” is “entirely absurd.”

>On labels/universes (FA2)
The quote “provocative/sensationalist/exoticist/apocalyptic narrative” about “suspending contradictions with labels” has “absolutely nothing to do” with reality. IUT uses standard labels for distinct objects; universes appear precisely as in SGA1 and derived functors; given Lean4’s handling of SGA1/derived functors, there is “no fundamental obstruction whatsover” to formalizing IUT. It will take years; so did everything else of substance.

>On “vulnerability” to label-removal
The critique “reflects a fundamental misunderstanding” since “no nontrivial set-theoretic mathematical structure … is ‘robust’ … to ‘arbitrary label-removals’.” Identifying 2 and 3 in N does wonders for arithmetic; alas, not the good kind.

>On set-theoretic paradoxes (FA3)
“It must [be] stated categorically” that prime-strips/theta-links do not trigger paradoxes; the issue is incompatibility with additive structure, leading to multiplicative or group-theoretic frameworks. “[math]\in[/math]-loops” are philosophical analogies.

>On splitting off an “anabelian core” from abc
Attempts to separate the anabelian/Teichmüller part from the abc application are “mathematically meaningless,” indeed “nothing more than a meaningless self-contradiction.” It is, inconveniently, the same mathematics.

>On taste-policing and ersatz IUTs
The practice of rewriting IUT to please outsiders is “particularly pernicious,” producing “logically unrelated fabricated versions … entirely devoid of any meaningful mathematical content.”