Post #1846797
2026-04-26 17:03 UTC
@zwarich YES!!! This was very frustrating.
He had this one thing that he would NOT stop saying, that it was an open problem whether MLTT was consistent with classical mathematics. It was ..... not an open problem. But he drummed up a lot of controversy and confusion over nothing, and this disinformation campaign probably led to some very questionable projects getting funded.
Replies (1)
-
@jonmsterling@mathstodon.xyz 2026-04-26 17:05
@zwarich To my recollection, he viewed the possibly unsoundness of type theory in classical mathematics as a special case of a more general problem that he claimed was open (his "initiality conjecture"), which was also not an open problem. (And even if it was an open problem, that would not have implied that the soundness was open.) This is of course separate from the weird PA-inconsistency talk that he gave. But I guess my point is, he said a lot of weird and damaging stuff.