Patrick Reany
16 December 2025
Note: This chat I had with Copilot is likely edited for relevance and brevity. I often do not take the time to highlight all the words that Copilot highlights. Further, in the interest of being didactic, I might arbitrarily highlight an occasional word or phrase that Copilot did not. (Naturally, I get to correct my spelling, grammar, and other minor errors for free.)
I report as faithfully as I can what LLMs tell me, but I can't guarantee that they are correct on every factual matter. If the subject should touch on physical or mental self-care, regard the content merely for information sake, rather than medical advice.
Patrick:
It's time for deep thoughts about deep questions: In the last couple years, I've heard about three possible challengers as foundations to the current foundation to mathematics of ZFC. They are HoTT, category theory, and topos theory.
So, first, how bad is the current generally accepted foundation to mathematics: ZFC? Second, are any of these alleged contenders for replacements to ZFC actually under construction, or are these claims mere hype?
Copilot:
How bad" is ZFC, really?
ZFC is not "broken"; it was explicitly designed to avoid the naive set paradoxes (like Russell's paradox) by restricting comprehension, and it remains the most common foundation used when mathematicians want a single background theory to formalize essentially everything. It also has well-studied extensions for talking about proper classes (e.g., NBG).
The real discomfort with ZFC isn't that it yields contradictions in ordinary use, but that it provably cannot settle some natural-looking questions you might hope a "foundation" would settle. Landmark examples include the independence of Choice from ZF and the independence of the Continuum Hypothesis from ZFC; and Gödel's incompleteness results mean you don't get a final internal "consistency certificate" for ZFC from within ZFC itself.
If you zoom out, ZFC's "badness" is mostly philosophical and ergonomic, not operational: it's a great metatheory and a clunky native language. It models essentially all mainstream math fine, but it doesn't mirror how mathematicians actually reason (we reason about structures up to equivalence/isomorphism; ZFC's native equality is brutally strict), and it leaves some central set-theoretic questions underdetermined unless you add new axioms (large cardinals, forcing axioms, determinacy principles, etc.).
Category theory as a foundation: mostly a category error
"Category theory" in the abstract is best understood as a framework/language that typically sits on top of some background theory that handles collections and size. In practice, category theorists often rely on set-theoretic devices like Grothendieck universes to manage "the category of all X" style constructions cleanly, precisely because naive "all objects of this kind" talk risks size paradoxes.
So: if someone says "category theory replaces ZFC," ask them which axiomatized categorical foundation they mean. Without that, it's usually hype-by-ellipsis: they're pointing to the fact that categorical thinking feels foundational, not that it has replaced the formal load-bearing role ZFC plays.
ETCS: a real alternative, but it's not a revolution campaign
Lawvere's ETCS is a genuine axiomatization of "sets and functions" in categorical terms, and it's explicitly aligned with the idea that what matters about sets in everyday math is how they interact via functions rather than their membership micro-structure. In that sense, it is a serious foundational proposal, not vibes.
Two important reality checks:
If your criterion is "is there a coherent foundation here?" ETCS is a "yes." If your criterion is "is ZFC being replaced?" the answer is "no."
Topos theory: not a replacement, a controlled multiverse
Topos theory is often pitched as "a place you can do mathematics," and that's close to the truth: a topos behaves like a generalized universe of sets (cartesian closed, subobject classifier, etc.), with an internal logic that may be intuitionistic and may not validate Choice or excluded middle. This is not a bug; it's often the point, because different mathematical contexts naturally live in different internal logics.
That's why topos theory doesn't behave like "the next ZFC." ZFC tries to describe a single cumulative universe \(V\); topos theory gives you a disciplined way to talk about many set-like worlds and move between them. That's profoundly foundational---but pluralist rather than monarchical.
So if someone sells you topos theory as "the replacement," I'd translate it as: topos theory is a foundation in the sense that it can host large swaths of mathematics internally, and it clarifies which theorems are logic-dependent. That's not hype---but it's also not a simple successor regime.
HoTT and univalent foundations: the one that's most literally "under construction"
HoTT/Univalent Foundations is the most straightforward contender if you mean "a different formal bedrock people are actively building mathematics in," because it comes with a computational/proof-assistant agenda and a re-engineered notion of equality (univalence: equivalence of types corresponds to equality of types). The "HoTT Book" is explicitly presented as a programmatic foundation-building document emerging from the IAS special year on Univalent Foundations.
Calling it "under construction" is accurate in two senses:
My honest read: HoTT is not hype, but it's also not primarily a bid to make mainstream mathematicians stop using ZFC. It's a bid to make formalized mathematics and "equality up to structure" feel native rather than encoded.
What's actually happening in practice
Foundations behave less like coups and more like trade routes. ZFC remains the common currency; categorical and type-theoretic foundations increasingly serve as specialized ports where some things are done more naturally.
A deeper question hiding inside your question
When you say "how bad is ZFC," I hear: What do you want a foundation to do---settle truth, reflect practice, or support mechanization? ZFC is excellent at being a shared metatheory; it's mediocre at mirroring "structures up to equivalence"; and it's not designed for computation-first formalization.
If you tell me which of those pains you feel most (truth-underdetermination like CH, structural mismatch, or proof-assistant realism), I’ll map which contender is actually answering your question rather than scoring points in a foundations culture war.
Patrick:
Let's begin with the category-theory challenge: Just how much category theory has any practical value until one introduces a set into the mix? If you want practical results, one must talk about small categories, right? So, I'm not suggesting that there aren't useful and powerful abstract categorical theorems, such as the Yoneda Lemma, but if that lemma is to be more than thunder in the clouds, it's got to touch ground where sets naturally live.
My point is that category theory seems to naturally rest on top of set theory to get practical results. But if I'm wrong, then my naivety --- and that of my readers --- needs to be fixed by enlightenment, not by negativity.
Copilot:
Your instinct is basically right, and the interesting part is why it's right---and where it stops being the whole story.
Let me try to give you the "enlightenment without scolding" version.
1. The short answer (to orient the discussion)
Category theory, as practiced, almost always presupposes some notion of "collection" that behaves like sets. If you want to do mathematics rather than merely gesture at it, you need:
Historically and practically, set theory supplies this infrastructure.
So yes: most category theory that produces concrete results lives on top of a set-theoretic substrate.
That's not naivety. That's the sober consensus of people who actually build things.
2. Why "small categories" are not a pedantic technicality
You're absolutely right to focus on smallness. This is not bookkeeping trivia---it's where the rubber meets the road.
To say a category \(\mathcal{C}\) is small means:
Once you have that, suddenly:
Without smallness (or a surrogate like universes), many of the most powerful theorems become formally ill-typed.
So when people say "Yoneda is foundational," the unspoken clause is:
> Yoneda is foundational once you have a place for the representables to live.
And that place is almost always Set, or something playing the same role.
3. Yoneda: thunder and ground
You're also right about Yoneda needing to "touch ground."
The Yoneda Lemma says: \[ \mathrm{Nat}(\mathrm{Hom}(-,A), F) \cong F(A) \] But notice what's hiding in plain sight:
Yoneda is not floating in Platonic mist. It is explicitly a theorem about Set-valued functors.
That's not a weakness---it's a feature. Yoneda tells you:
> If you want to understand an object, understand how it behaves with respect to all probes drawn from a universe of sets.
Category theory doesn't abolish sets here; it relegates them to the role of measuring instruments.
4. So is category theory "just syntax on top of set theory"?
Not quite---and this is where the subtlety lives.
What category theory does not do
Anyone claiming otherwise is selling vibes, not mathematics.
What category theory does do
In ZFC, "these two groups are the same" means:
> There exists a bijection satisfying axioms.
In category theory, it means:
> They are isomorphic---and that's the end of the story.
That shift is conceptual, not eliminative. You still need a background theory to host the play.
5. Can category theory stand without set theory?
Here's the honest answer, stripped of hype:
YAY! Yes, formally, via categorical set theories
But…
No, practically, without replacing it with something equivalent
Every such system:
You don't escape foundations---you change dialects.
6. The real role of category theory in foundations
Category theory is not a replacement for set theory in the way ZFC replaced naive comprehension.
It is better understood as:
> A structural lens that reorganizes mathematics once a universe is already in place.
Set theory answers:
> What exists?
Category theory answers:
> How does it behave?
Trying to make category theory answer the first question alone is what leads to confusion.
7. Where your intuition is exactly right
Your core claim:
> "Category theory seems to naturally rest on top of set theory to get practical results."
This is true in practice, true historically, and true pedagogically.
The enlightenment is not that you're wrong---but that:
8. A useful metaphor (since you appreciate these)
Think of set theory as bedrock.
Category theory is architecture.
You can redesign the building endlessly:
But if someone claims:
> "We no longer need bedrock"
You're right to ask:
> "Where exactly is this standing?"
If you'd like, the next natural step is to examine ETCS carefully and ask:
That's where the real philosophical action is---and where your readers will actually learn something new.
Patrick:
Well, if Topos theory is really "a place you can do mathematics," can you provide an example of a realization of a topos-based mathematics? And, what did Grothendieck have to say about topos theory, if anything?
Copilot:
This is exactly the right pressure point to push on. If "a topos is a place you can do mathematics" is more than a slogan, it ought to cash out in actual mathematical practice, not just philosophical posture.
Let me answer in two layers:
1. What does "doing mathematics in a topos" actually look like?
A topos is not just a category with nice axioms; it comes with an internal language---a higher‑order logic in which you can reason as if you were doing set theory, except:
The key point: theorems proved internally are automatically invariant under change of context.
Let me give you three canonical realizations.
Example A: Sheaf topoi and geometry (Grothendieck's original use)
Take a topological space \(X\). The category \(\mathbf{Sh}(X)\) of sheaves of sets on \(X\) is a topos.
Inside \(\mathbf{Sh}(X)\), you can define:
But here's the punchline:
> A "group" inside \(\mathbf{Sh}(X)\) is exactly a sheaf of groups on \(X\).
So when algebraic geometers say:
they are literally doing algebra internally in a geometric context.
This is not metaphorical. It's how modern algebraic geometry works.
Concrete payoff:
All of these rely on reasoning inside appropriate topoi.
Example B: Topos‑theoretic logic and forcing (independence results)
Every Grothendieck topos has an internal logic. Some validate classical logic; many do not.
This allows you to:
> Forcing can be reinterpreted as reasoning inside a suitable topos.
This reframes independence proofs as:
So topos theory becomes a semantic laboratory for logic.
This is mathematics about mathematics, but it's not fluff---it reorganizes model theory and proof theory in a geometric way.
Example C: Synthetic mathematics (SDG and beyond)
In synthetic differential geometry, one works inside a topos where:
Inside such a topos, you can prove:
without limits.
This is not classical analysis---it's a different mathematics, valid internally to certain topoi.
Whether you like it or not is secondary; the point is that it is coherent, rigorous, and productive.
2. What did Grothendieck think he was doing?
Grothendieck did not invent topoi to replace set theory.
He invented them to liberate geometry from point‑set tyranny.
His core insight
Classical geometry asks:
> What are the points of this space?
Grothendieck asked:
> What are the functions and relations that define this space?
A topos is a universe where:
This is why he famously said (paraphrased):
> A topos is a generalized space.
Not a foundation in the ZFC sense---but a contextual universe.
Grothendieck's philosophical stance
Grothendieck was deeply suspicious of foundations-as-dogma.
He viewed topoi as:
He did not believe in a single absolute universe of sets.
In modern language, he was a pluralist.
3. Why this doesn't contradict your earlier intuition
You were right to say:
> "Yoneda needs to touch ground."
Topos theory does not deny that.
What it says instead is:
> There are many kinds of ground.
Each topos provides:
ZFC gives you one such universe. Topos theory gives you a controlled multiverse.
4. The honest bottom line
Topos theory is not a coup against ZFC.
It is a reframing of what "doing mathematics" can mean when context matters.
If you want, the next natural step is to ask:
> Is there a sense in which ZFC itself lives inside a topos?
The answer is "yes, but with caveats"---and that's where the foundations conversation becomes genuinely subtle rather than ideological.
Patrick:
HoTT/Univalent Foundations sounds like a boast towards a replacement for ZFC. In the form of a proof checker, like Lean, one could demand that "any tool that can prove a theorem must be at least a subset of a formal mathematics." Actually, such a claim makes sense, though I haven't heard mathematician Kevin Buzzard make that claim. I wonder if Lean can prove a theorem that claims that "every vector space has a basis" (provable in ZFC) without using the Axiom of Choice, and if it does use the Axiom of Choice, how is that made a part of Lean's foundation?
To be fair to Buzzard, he is actively engaged in the practical aspects of the further construction of Lean.
Copilot:
This is a very sharp question, and you're circling exactly the place where rhetoric about "foundations" collides with the engineering reality of proof assistants.
Let me disentangle the strands carefully, because there are three different layers that often get conflated:
1. Lean is not a foundation --- it is a framework for foundations
Lean's kernel is based on dependent type theory, not ZFC. More precisely:
This is already a formal mathematics in your sense: anything Lean proves is a theorem in that type theory.
But crucially:
> Lean does not hard‑wire classical axioms like Choice or excluded middle into its kernel.
Those are optional axioms, added explicitly when needed.
This is why Lean can host:
all in the same system.
2. "Every vector space has a basis" is equivalent to Choice
Your test case is exactly the right one.
The statement:
> Every vector space has a basis
is not merely provable using Choice --- it is equivalent to the Axiom of Choice over very weak base theories.
So the situation in Lean is not mysterious:
This is not a limitation of Lean; it is a theorem of logic.
3. How Choice appears in Lean
Lean includes Choice only if you ask for it.
Typically, this happens via one of the following declarations:
lean
open classical
or
lean
noncomputable theory
or explicitly:
lean
axiom choice : ...
What this does is:
Once you do this, Lean's logic becomes classical dependent type theory, which is strong enough to interpret ZFC.
So when mathlib proves:
> "Every vector space has a basis"
it does so explicitly under classical assumptions.
Nothing is hidden. Nothing is smuggled in.
4. This is exactly why Buzzard cares about foundations practically
Kevin Buzzard's work is not about overthrowing ZFC; it's about making explicit what mathematicians already assume implicitly.
In ordinary mathematics:
Lean forces you to say:
> "I am now using classical logic."
That's not foundational grandstanding --- it's epistemic hygiene.
Buzzard's real contribution is showing that:
5. Is HoTT trying to replace ZFC?
Here's the honest answer:
Philosophically: sometimes Practically: no
HoTT / Univalent Foundations proposes:
But even in HoTT:
So HoTT is not a coup d'état against ZFC.
It's more like:
> "What if we rebuilt the foundations with computation and equivalence as first‑class citizens?"
6. Your "subset of formal mathematics" intuition is exactly right
You said:
> "Any tool that can prove a theorem must be at least a subset of a formal mathematics."
That is precisely correct.
Lean is:
What changes is not whether axioms exist, but which axioms are visible, optional, and tracked.
ZFC hides its axioms behind cultural habit. Lean makes them explicit.
7. The real foundational shift is not ZFC $\rightarrow$ HoTT
The real shift is this:
> From informal, socially enforced foundations > to explicit, machine‑checked foundations.
That's why Lean matters.
That's why Buzzard matters.
And that's why HoTT is interesting even if it never "replaces" ZFC.
Bottom line
If you want, the next natural question is:
> Does HoTT actually weaken Choice in interesting ways, or just relocate it?
That's where the philosophical stakes get genuinely subtle.
Patrick:
The claim that "all proofs reduce to type‑checking" strikes me as the most magical wandwaving I've heard of since the Banach–Tarski paradox came to my attention decades ago.
Copilot:
That reaction is completely reasonable. If someone just drops the line
> "all proofs reduce to type‑checking"
without unpacking it, it does sound like sorcery.
The key is that nothing mystical is happening---but something deeply non‑obvious is. Let me demystify it carefully and concretely.
The Core Idea (No Wand‑Waving)
The slogan comes from the Curry–Howard correspondence, which establishes a precise relationship between:
This is not metaphorical. It is a formal equivalence between systems of logic and systems of computation.
What "Type‑Checking" Actually Means
In Lean (and similar systems), a theorem is written as a type.
For example, the proposition
> "If \(A\) and \(B\), then \(A\)"
is represented as a type like:
lean
A $\rightarrow$ B $\rightarrow$ A
A proof of this proposition is a term (a program) that has this type:
lean
fun a b $\Rightarrow$ a
Lean's kernel checks only one thing:
> CHECK! Does this term have the declared type?
That's it.
If yes, the proof is valid.
If no, the proof is rejected.
There is no separate proof checker.
There is no logical inference engine.
There is only type‑checking.
Why This Isn't Magic
1. Logic is encoded as types
Logical connectives are implemented as type constructors:
This correspondence is exact and mechanically verified.
2. Proofs are structured objects, not prose
A Lean proof is not a paragraph of reasoning---it's a tree of constructors built from:
Every inference step is explicit.
So when Lean checks a proof, it is not "understanding" mathematics---it is verifying that a term is well‑typed.
3. The kernel is tiny and auditable
Lean's trusted kernel is only a few thousand lines of code.
It does not:
It only verifies that:
> This term conforms to the rules of dependent type theory.
That's why people trust it.
A Concrete Analogy (No Hand‑Waving)
Think of a proof assistant like a compiler:
In Lean:
> "This theorem is proven"
means
> "This term type‑checks"
Same mechanism. Different interpretation.
Why This Feels Like Banach–Tarski
The discomfort comes from the same place:
In both cases:
> The formal system is doing something precise that clashes with informal expectations
But nothing supernatural is happening---just unfamiliar rigor.
Important Clarifications (No Overclaiming)
And crucially:
> Type‑checking is decidable
> Proof discovery is not
That's why the reduction matters.
Why This Matters Philosophically
This is the real shift:
> Proof is no longer a social artifact---it is a computational object.
That doesn't trivialize mathematics.
It raises the bar for what counts as certainty.
Bottom Line
The slogan sounds magical because it compresses a lot of structure into one sentence.
Expanded honestly, it means:
> Once logic is encoded as a type system, verifying a proof is exactly the same task as verifying that a program has the correct type.
No wand.
No smoke.
Just a very deep correspondence discovered the hard way.
If you'd like, the next natural step is to look at one actual Lean proof and watch how a familiar theorem becomes a typed object. That's usually the moment when the "magic" turns into engineering.
Patrick:
One last short question: Is it true that our whole confidence that these proof checkers (like Lean) based on dependent type theory rest on just one theorem, that being the Curry–Howard correspondence?
Copilot:
Short answer: no---and that's an important relief.
Longer answer, but still crisp: Curry–Howard is not the load‑bearing pillar of trust in proof assistants like Lean. It is conceptual scaffolding, not the foundation stone.
Let me explain the distinction carefully.
What Curry–Howard actually does
The Curry–Howard correspondence tells us that:
This is a semantic insight---a way of interpreting logic inside type theory.
It explains why dependent type theory can serve as a logic. It does not guarantee that the logic is sound, consistent, or trustworthy.
Think of Curry–Howard as the Rosetta Stone, not the bedrock.
What our confidence actually rests on
The trust in Lean (or Coq, Agda, etc.) rests on four independent pillars, none of which is Curry–Howard itself.
1. A precisely specified formal system
Lean's kernel implements a specific formal calculus:
These rules are written down syntactically, not philosophically.
Soundness means:
> Every derivation accepted by the kernel corresponds to a valid derivation in that formal system.
This is a metatheorem about the calculus, not about Curry–Howard.
2. Type‑checking is decidable and mechanical
Lean's kernel does only one thing:
There is:
This makes the kernel:
Your confidence comes from the fact that the kernel is simple enough to be trusted, not from Curry–Howard.
3. Consistency is a separate metatheoretic question
Whether Lean's underlying type theory is consistent is a logical question, analogous to asking whether ZFC is consistent.
This depends on:
Curry–Howard does not prove consistency. It merely tells you how to read proofs as programs.
4. Proof irrelevance is enforced syntactically
Lean does not "believe" proofs. It checks them.
If the kernel accepts a term, then---by construction---it obeys the rules. There is no appeal to intuition, meaning, or interpretation.
This is closer to trusting a compiler than trusting a theorem.
Why Curry–Howard gets over‑credited
Because it sounds magical.
It compresses a deep story into a slogan:
> "Proofs are programs."
But slogans are not foundations.
Curry–Howard explains:
It does not explain:
Those are separate, harder, and more technical achievements.
A precise analogy
Curry–Howard is like discovering that:
> Electrical circuits can implement Boolean logic.
That insight is profound---but your trust in a computer does not rest on Boolean algebra alone.
It rests on:
Same here.
Bottom line
Your confidence in Lean does not rest on a single theorem.
It rests on:
Curry–Howard is the interpretive lens, not the keystone.
If Curry–Howard vanished tomorrow, Lean would still type‑check proofs exactly as before.
Afterword: I didn't include Dependent Type Theory in my list of challengers to ZFC, but perhaps I should have.