Exomnium

@mouse_math comes to set theory. Consider how freely people are will to insinuate or outright say that set theory is 'not mathematics'.

@mouse_math Well (a) model theory actually has quite a few points of contact with mainstream mathematics (e.g., o-minimality, operator algebras via continuous logic) and (b) I feel like there are other analogously isolated parts of math that don't get the same treatment, especially when it

what's the most annoying field of mathematics?

@mouse_math I'm a mathematical logician and I often feel like an outsider in mathematics more broadly because there's a pretty consistent level of disdain directed towards my field from people in more popular areas of math. I'm not sure whether that makes me daft or just a stroll.

@Exomnium there's hundreds of fields of math, with distinct objectives, problems, techniques; a student of math is attracted to some and repelled by others. i am curious what different people think. what is the point of your kind of question? are you daft or just a troll?

@mouse_math I just think that the kind of social negativity this kind of question tends to bring out doesn't really accomplish anything.

@mathandcobb It is incredibly naive to think that this is not a realistic concern.

@mathandcobb The fear is not about what would happen in an ideal world. The fear is about how this could change the political reality of funding for mathematics.

I, for one, I'm telling students it's perhaps the most exciting time to be a mathematician, quite possibly in the history of mathematics. All of a sudden we are given a tool that can help us make huge leaps! How could anyone see this as our profession dying? Embrace it. Learn how to use it, empower yourself, and profit.

‼️🚨 ALARMING: Google now treats privacy as suspicious behavior by default. Users of GrapheneOS, CalyxOS, /e/OS, and other deGoogled Android phones are being locked out of millions of websites unless they install the exact Google Play Services software they deliberately removed. GrapheneOS is recommended by the EFF and used by journalists, lawyers, and activists in high-risk environments. The audience most likely to read Google's data practices and refuse its terms is now flagged as fraudulent for that exact decision. What happened?: ▪️ Google announced "Cloud Fraud Defense" at Cloud Next on April 22-23, 2026, branding it "the next evolution of reCAPTCHA." Existing reCAPTCHA customers were auto-migrated. ▪️ When the system flags traffic as suspicious, the old click-the-bus puzzle is gone. Users get a QR code instead. ▪️ Scanning the QR code requires Google Play Services running on the device. Internet Archive snapshots show this requirement has been live since at least October 2025, silently rolled out for 7 months before anyone noticed. ▪️ No Play Services = no QR scan = locked out. The bigger picture: ▪️ Google already tried this in 2023. It was called Web Environment Integrity (WEI), and it would have let Google decide which devices were "real enough" to access the web. Standards bodies and the public pushed back hard, and Google killed it. Three years later, the same idea is back, just hidden behind a QR code instead of a browser feature. ▪️ reCAPTCHA runs on millions of websites. Every developer who keeps using it is now, by default, telling deGoogled Android users they're not welcome...

@jdlichtman I find it really weird that the co-sponsors of this symposium (the Futures of Mathematics Institute) has literally no online presence at all, especially given the fact that it's a 501(c)(3).

@wolajacy @ElliotGlazer While some of these results have good proofs in, say, topos-theoretic language, many of them, especially those involving inner models, seemingly do not, despite 40+ years of people like Mac Lane and Lawvere claiming that set theory has been obviated by category theory.

@Exomnium @ElliotGlazer It was an honest question. Who borrows more is not a very good benchmark (if a field is "abstract nonsense" then it obviously wouldn't be interested in borrowing from more down to earth fields).

Set theory advance of the decade imo. Will very likely lead to a refutation of the common conjecture that MM is equiconsistent with a supercompact cardinal.

@wolajacy @ElliotGlazer Gödel's L can be used to show that the existence of a Boolean topos entails the existence of a Boolean topos satisfying choice.

@wolajacy @ElliotGlazer The vast majority of metamathematical results from set theory entail direct corresponding results in type- and category-theoretic foundations. The proof of the independence of CH from ZFC can be used to prove the independence of CH from DTT + choice.

@wolajacy @ElliotGlazer This is such an obnoxious attitude. Type theory research borrows far more ideas and results from set theory research than the other way around.

@ElliotGlazer (As opposed to doing foundations of mathematics in type theory, proof theory, categorical programming languages semantics etc.)

@ModalMetamodel (ii) Any model satisfying this condition is strongly κ-homogeneous (Hodges Theorems 10.4.4 and 10.4.5). (iii) For any ordinal γ such that No_γ is a model of RCF, any field automorphism of No_γ has a canonical definable extension to all of No.

@ModalMetamodel You need three components: (i) For any cardinal κ and ordinal α, there is an ordinal β > α such that No_β is a special model of RCF (in the sense of Chapter 10 of Hodges) satisfying cf(|No_β|) > κ.

Just how ‘rigid’ is the surreal line (as an ordered ring)? For instance, for any two surreals a and b above all standard integers, does an automorphism taking a to b exist? It seems that this’ll be somewhat dependent on the availability of global choice and such.

@ChrSzegedy @mathLOb C is in the body of the formula in the subscript of n_C. Also, if you read the proof, you can see that A just needs to be large enough for n_{9 + 2^i 3^j} in the second sum to be well-defined.

@mathLOb The formula does not contain A and C. That's sus.

Hanson, Watson: A formula for any real number, maybe arxiv.org/abs/2602.02384 arxiv.org/pdf/2602.02384 arxiv.org/html/2602.02384

@_chenson__ @ElliotGlazer Yes that's right. The last argument passed to `addDeclCore` is telling it to skip type checking.

@ElliotGlazer Am I correct that this calls `addDeclWithoutChecking`? So if you replay the environment, this will correctly be caught as a kernel error?

Congratulations to my good ol' pal and colleague James Hanson for successfully proving Fermat's Last Theorem in Lean, using only one standard axiom (propext).

@JasonRute @ElliotGlazer @leanprover This is an example of 'environment hacking' and I believe it's not really considered a bug by the developers per se. Here's a link to the original Zulip thread that discusses this: #narrow/channel/113488-general/topic/PSA.20about.20trusting.20Lean.20proofs/near/392684837" target="_blank" rel="nofollow noopener">leanprover.zulipchat.com/#narrow/channe…

@ElliotGlazer I’m really confused. @leanprover can you clarify? First is this a true soundness bug in the kernel or a just a UI bug? Is there a GitHub issue or a Lean Zulip post about this issue?

@JasonRute @ElliotGlazer There really haven't been any 'killer applications' of CT in ST that would get people over those grudges. The only thing on my radar is Espíndola's claimed topos-theoretic proof of Shelah's eventual categoricity conjecture, but that's a fairly niche topic to begin with.

@ElliotGlazer Do set theorists and categorical logicians (studying say toposes or models of type theory) still have deep-seated divisions? I hope not, since I imagine a lot of connections and cross over there, especially when you consider removing axioms from ZFC.

When my colleague in the set theory research discord asks for projects that will improve rather than worsen set theory's public reputation: