Consistency strength bounds from Lean proofs

Stream: maths

[James E Hanson]

As is old news at this point, Sky Wilshaw recently formalized Randall Holmes's proof of the consistency of $\mathsf{NF}$ in Lean. If I recall correctly, Holmes has stated that he believes the proof should go through in something as weak as $\mathsf{ZFC}$ without replacement + "$\beth_{\omega_1}$ exists", and this is plausible to me given my extremely broad understanding of the proof. But I'm also under the impression (and please correct me if I'm wrong) that, while you can ask Lean to report the axioms used in a proof, this is really in the sense of the word 'axiom' used in type theory, rather than in classical mathematical logic, and as such doesn't necessarily represent the full strength used in a proof. (For instance, a fully constructive proof of the consistency of $\mathsf{PA}$ would be reported as using no axioms.)

It's relatively clear to me that one could read off the number of universe levels used in a fully compiled proof term, but a priori it seems like this wouldn't allow you to get below something like $\mathsf{ZFC}$ + "there exists approximately $1$ inaccessible cardinal", which is well above Holmes's intuition about how much strength his proof really needs. Has there been any work that would allow one to extract a tighter bound automatically? I think this would be nice to see even if it can't get as low as Holmes's estimate.

I'd also be curious about this in the context of the proof of Fermat's Last Theorem, since the original proof famously uses some inaccessible cardinals (i.e., Grothendieck universes) but it's known that the relevant machinery needs much less and it's widely suspected that the theorem should be provable in $\mathsf{PA}$.

[Jason Rute]

This PA.SX question addresses a bit of this with links back to Zulip: https://proofassistants.stackexchange.com/questions/2728/lean-and-inaccessible-cardinals/2755#2755

[Jason Rute]

But Lean isn’t probably ever suited for measuring below the strength of ZFC.

[Jason Rute]

Here is a direct link to a Zulip thread also talking about related stuff: https://leanprover.zulipchat.com/#narrow/stream/236446-Type-theory/topic/Theory.20of.20Lean.20with.20n.20universes

[Kevin Buzzard]

I'd also be curious about this in the context of the proof of Fermat's Last Theorem, since the original proof famously uses some inaccessible cardinals (i.e., Grothendieck universes)

Just pushing back on this -- it was a completely incorrect rumour at the time that the original proof "famously" used inaccessible cardinals. The proof used nothing beyond SGA4.5 which needs no inaccessible cardinals, and it was just a bunch of misguided logicians making a lot of noise. The facts that results from SGA4 appear in the FLT paper and that parts of SGA4 use inaccessible cardinals cannot be used to deduce that FLT uses inaccessible cardinals (this was the error made by the people who just looked at the references and didn't understand the proof).

[James E Hanson]

Kevin Buzzard said:

and it was just a bunch of misguided logicians making a lot of noise.

Professor Buzzard, I must confess that as a logician myself I find the way you phrase these things a little unwelcoming.

I would presume that after you finish formalizing FLT, you'd like to be able to point to some computer verification of the additional mathematical fact that the proof of FLT does not need any inaccessible cardinals (otherwise how could you be so certain that it actually doesn't?). At the end of the day, that is what I'm thinking about. To what extent can we automate the fairly common 'obvious' process of looking at a proof and deciding that it doesn't depend on strong assumptions in the background theory?

From what I'm gathering, though, this might be hard to do automatically from a proof formalized in Lean, as dependent type theory tends to use inaccessible cardinals a little bit liberally. I guess I need to spend some time thinking about when and how you can systematically replace something like Grothendieck or type-theoretic universes with smaller 'approximate universes' (like how the Stacks project operates to stay inside $\mathsf{ZFC}$). This is pretty interesting to me because we know that you can't actually do it in full generality, since, for instance, $\mathsf{ZFC}$ + "there exists an inaccessible cardinal" proves $\Pi^0_1$ facts that $\mathsf{ZFC}$ alone does not. This makes it a challenge to delineate, say, a Lean proof of $\mathrm{Con}(\mathsf{ZFC})$ from a Lean proof of FLT, since these are both $\Pi^0_1$ statements.

[Kevin Buzzard]

Yes my proof of FLT will use inaccessibles, because of the nature of the software I'm using. Wiles' proof did not and that's a fact, and I apologise if I explained this in an unwelcoming way but it makes me angry that this lie is still being perpetrated.

[Kevin Buzzard]

To be more precise, my proof will be a proof in Lean's type theory, which is equiconsistent with ZFC + a statement about inaccessibles

[Kevin Buzzard]

@Mario Carneiro has thought about the idea of post-processing lean proofs to demonstrate that they "could have been done without inaccessibles" but apparently this is hard to do in practice because universes are everywhere in the theory.

[Jason Rute]

@Kevin Buzzard Just so I’m clear, you are saying that if one looks at the original proof of Wiles’ theorem and all the specific theorems that it references from other sources, then none of this used large cardinals? And if someone bothered to check that, it would have been clear? (And of course to be fair to McLarty, going through FLT’s proof in detail just to work this out may have been a research level task on its own. :slight_smile:)

[Jason Rute]

(Maybe I shouldn’t defend McLarty. I’ve never read his paper and I don’t know if he was right or not on his points, especially about FLT, at least on the surface, using universes.)

[Kevin Buzzard]

McLarty proved much more because he showed that one needed far less than ZFC. But yes, Wiles never uses universes and nor does anything he relies on.

Wiles does use etale cohomology. The very first references for etale cohomology were Grothendieck's SGA4 and SGA5 which famously use universes because they develop a hugely general machine using topoi which could be used to construct all sorts of exotic cohomology theories, for example fpqc cohomology which does have foundational subtleties. However etale cohomology was then used to prove the Weil conjectures and in order to demonstrate to the mathematical community that universes were not used in the proof of the Weil conjectures, Deligne wrote SGA4.5, which developed etale cohomology without all the topos-theoretic framework and demonstrated that the proof of the Weil conjectures did indeed work fine in ZFC. The situation then stayed like this for 20 years, and several other books were written developing etale cohomology in ZFC for example Milne's book and Freitag-Kiehl.

Then suddenly when FLT was proved someone claimed on the internet that the proof used etale cohomology and hence universes, and despite the attempts of several number theorists to try and explain that this was not at all the case, the claim still seems to have some traction.

[Mario Carneiro]

well this sounds like a rather disappointing end to the project to show that the lean proof of FLT doesn't use universes

[Kevin Buzzard]

Yes it's just the opposite! I'm putting them back in!

We talked about this sort of thing in about 2019. My memory of the conversation was that I said "presumably I can just use universes left right and centre in any proof, and then you can write a program checking that the proof works fine in ZFC" and you said "hmm it might not be that simple". And then later on you did write a simpler program which counted the number of universes used in proofs, and the answers were far higher than I was expecting, e.g. there was some trivial assertion about finite sets which you claimed used Type 4 at some point (and I was incredulous but it was what your code said). This was all in Lean 3 and then when Lean 4 happened I encouraged you to port the code but you had plenty of other things to worry about (e.g. porting mathlib) so as far as I know we still don't have it. But that code (just counting the number of universes actually used) isn't what would be needed here, what would be needed here is far more nontrivial and probably we're not ready for it yet. @Joël Riou has been thinking about this sort of thing carefully in some of his recent PRs in category theory. The general phenomenon that you want to take care of is when you want to define a cohomology theory by taking some kind of limit over covers but that limit is not a set. In SGA4 Grothendieck just took the limit anyway, and his cohomology group was defined one universe level up. In SGA4.5 Deligne showed how you could take the limit over a set and still get the same answer (that's the basic idea but it's more complicated than this, you also have to show that everything you want to do with the cohomology theory also descends, but this is the basic idea). Joel has been proving general results of the form "if hom types in a category descend to a smaller universe then various constructions which you make using this category also descend". But if you want to get a proof of FLT into ZFC then you need to show that these techniques apply. Set theorists understand this problem well; a reference for how it works in algebraic geometry is in the Stacks project: the set-theoretic input is here and the application to schemes is here. In particular it's not something which you get "for free", there is content here.

I suppose the last thing to add is that ironically the work I'm formalizing (the modern version of the Wiles paper) will avoid etale cohomology completely. However I will be assuming the existence of Galois representations attached to Hilbert modular forms and the only known construction of these in the generality I require uses etale cohomology.

[Mario Carneiro]

Just to clarify, the project I'm talking about is an extension of that discussion we had (and also some discussions we had last summer at the hausdorff institute). The basic idea is that yes, you can count up the Type levels directly used in the proof and you will get a number like 4 or something and this can indeed be used to prove that you can establish the theorem using 4 universes, but that's a boring upper bound. It's possible to do better than that, even without changing the actual proof. @James E Hanson hints at this already in his first post, it is possible to interpret Type u as being less than a full universe and thereby avoid needing an inaccessible cardinal.

But if FLT itself (the original proof) doesn't use universes, then this is a much less interesting headline ("formalizing the proof in lean solved an open question about whether FLT can be done without universes") and instead is "formalizing the proof proved a weaker result and wasted a bunch of peoples' time"

[Damiano Testa]

In case it is useful to anyone, here is a 14 years old discussion of the same issue on mathoverflow: https://mathoverflow.net/questions/35746/inaccessible-cardinals-and-andrew-wiless-proof.

[James E Hanson]

Kevin Buzzard said:

but it makes me angry that this lie is still being perpetrated.

I apologize for spreading a misconception, but, again, the word 'lie' is pretty strong and accusatory. It suggests malicious intent.

Given the prevalence of people who seem to think that set theory 'isn't really mathematics' or something to that effect, I don't see what's wrong with set theorists being excited about the potential relevance of concepts in their field to big famous results. I've met people who work with Grothendieck universes and don't even realize they're directly related to the large cardinals set theorists talk about.

[Kevin Buzzard]

Thanks for coming back James. As you can see I clearly have very strong opinions about this (I remember it all unfolding at the time and being extremely frustrated about how incorrect claims were being circulated) but I think the mathoverflow post summarises the facts accurately.

Regarding the far more interesting question of how lean fits into all of this, my initial naive model of how things could work would be that we could just work in Lean's type theory and get on with it and then try and shoehorn it all into ZFC later on. But this is more subtle than it looks. I don't claim to understand all the subtleties but here is I think one, which I'll illustrate by example.

The concept of finiteness in ZFC is represented by a predicate on sets which can be captured by a formula. The concept of finiteness in lean is simply a function from a type universe to Prop. In ZFC you can do certain things with functions and you can do different things with predicates on sets, they're different objects and satisfy different rules. A class in ZFC can't be defined as just "any old collection of sets", it must somehow be defined by a rule. But you can say "let f be any old function". My worries about translating a proof of FLT in lean directly into a ZFC proof is that at some point I will use the language of categories and will do things which, to check they're ok in ZFC, one will have to take various definitions apart to check that they can be translated into predicates which can be expressed in an appropriate first order language and that I didn't do "functiony" things which can't be translated into "predicatey" things. For example I can say "choose a well-ordering of the reals" in ZFC but in lean I can say "choose a well-ordering of Type" because it's no different.

[Mario Carneiro]

The point is that "choose a well-ordering of Type" is also something you can do in ZFC, because Type is just another set. It's definitely got to be interpreted as a set, interpreting it as V doesn't work. Either you say that the set is a grothendieck universe and now you need an inaccessible cardinal (this is the easy way), or you interpret it as an almost-universe and check that the proof doesn't do any concrete construction that violates the almostness of the universe. I believe this is a more sophisticated version of your point about translating the proof into functiony things and predicatey things. But I am quite confident in asserting that the upshot for you is that should just "get on with it and then try and shoehorn it all into ZFC later on".

[Mario Carneiro]

I do think that this leads to an interesting problem for set theorists, namely to figure out what kind of almostness one needs to cover a significant fraction of lean in practice. As you know, I've been trying to figure that out myself, and I have some possible answers but they aren't great. Perhaps I can interest some other people in this problem.

[Kevin Buzzard]

Yes my model was "Type is the universe"

[Mario Carneiro]

That doesn't work because as you hint at, lean is able to do higher order things with Type that go beyond what ZFC can support

[Mario Carneiro]

even without using Type 1

[Kevin Buzzard]

I'm just not convinced that I do any of them

[Kevin Buzzard]

But this might be hard to check

[Mario Carneiro]

You certainly do. Just writing down Group requires defining a function into Type

[Kevin Buzzard]

But my point is that set theorists can talk about groups so I'm not really doing it

[Kevin Buzzard]

Just like how Wiles' proof doesn't really use universes

[Mario Carneiro]

I certainly agree with this, but that's basically what this almostness is about

[Mario Carneiro]

the challenge is to take that general intuition and make a coherent system out of it which isn't foiled every time you make a function type

[Mario Carneiro]

because lean really likes making function types

[Mario Carneiro]

and I'd like to try to reach a bit further and also handle "benign" uses of things like the category of sets, which are also not really fundamentally different from this idea that using Group doesn't mean any more than fancy notation for predicates

[Kevin Buzzard]

When discussing the ZFC question in the 90s it was clear that all the representable functor stuff in the deformation theory part of Wiles' argument could be shoehorned into an exposition which never said the word "category" at all, but the price you paid was a loss of readability which nobody wanted to pay.

[Mario Carneiro]

I think the approach I'm advocating will do much better than that, I think it won't require eliminating categories at all from the lean proof

[Mario Carneiro]

in effect, all of that elimination work is turned into an automated check and a metatheorem

[Mario Carneiro]

and if it works I think it will be a great advert for the advantage of having formal proof objects to begin with

[Edward van de Meent]

I wonder if this question translates to the existence of a metaprogram which maps definitions into ZFSet and predicates on them, in a "faithful" way

[Antoine Chambert-Loir]

Maybe this is implicit in the thread, but in his lectures at Collège de France, Thierry Coquand insisted that the basic Martin-Löf type theory, with universes, is weaker than second order Peano arithmetic. I understand from this that universes in type theory and Grothendieck universes in set theory are not strict analogues, so that eliminating Grothendieck universes from Wiles's proof shouldn't require to eliminate type theoretical universes from its formalization in Lean.

[Jason Rute]

But I assume that quote is referring to MLTT without axioms. The choice axiom makes a large difference.

[suhr]

MLTT is predicative, so it's much weaker than CIC used in Lean.

[Jason Rute]

I should know this, but what does predicative mean again? Is it basically that CIC has Prop and \forall X : Type, p X is in Prop for p : Prop? (I’m having trouble following https://proofassistants.stackexchange.com/questions/326/what-is-predicativity .)

[suhr]

You have this rule:

$$\frac{ Γ ⊢ {\color{red}σ}: \mathcal U_i \qquad Γ,({\color{red}x}: {\color{red}σ}) ⊢ {\color{red}τ}: \mathcal U_j }{Γ ⊢ (∀{\color{red}x}:{\color{red}σ}.\; {\color{red}τ}): \mathcal U_k},\quad k = imax(i,j)$$

In MLTT imax is simply max. In Lean it's different: https://lean-lang.org/doc/reference/latest//The-Type-System/Universes/#level-expressions

[suhr]

(outside of type theory predicativity might mean something completely different)

[Mario Carneiro]

I find it rather less likely that one can automatically remove uses of impredicative Prop from a proof of FLT in lean

[James E Hanson]

Kevin Buzzard said:

Thanks for coming back James. As you can see I clearly have very strong opinions about this (I remember it all unfolding at the time and being extremely frustrated about how incorrect claims were being circulated) but I think the mathoverflow post summarises the facts accurately.

Rather than just brushing off what I said, would you be willing to actually retract your insinuation that the statements in question were 'lies'?

[James E Hanson]

suhr said:

(outside of type theory predicativity might mean something completely different)

I wouldn't go so far as to say they're completely different. They all trace their roots to Russell's analysis of the paradoxes of naive set theory. But the senses of the word used in type theory and in classical mathematical logic are different enough to be somewhat incompatible, though, and it can be confusing.

[James E Hanson]

Mario Carneiro said:

It's definitely got to be interpreted as a set, interpreting it as V doesn't work.

If the operations being performed on Type are sufficiently predicative, could it not be possible to interpret it as something like the class of canonical codes for $\Sigma_n$-definable classes?

[Kevin Buzzard]

@James E Hanson I'm sorry I used the word "lie"and I'm sorry I upset you. The claim that Wiles' proof used large cardinals is an incorrect statement but I'm sure you made the statement without the intent to mislead. I'm happy to take any further discussion of this to DMs.

[Fernando Chu]

I may be mistaken but it was my understanding that if one can prove a statement in (ZFC + n inaccessible cardinals) that don't mention the inaccessible cardinals, then you can also prove this in ZFC (source). So if the Lean proof of FLT only uses n inaccessible cardinals, then this gives a true statement in ZFC+, which gives a true statement in ZFC with no extra cardinals, right?

[Mario Carneiro]

No, this is not true, ZFC + n inaccessibles is strictly stronger in consistency strength

[Fernando Chu]

Even for statements not involving the inaccessibles? Is the theorem mentioned in the link wrong, or is my understanding of it wrong?

[Mario Carneiro]

the consistency of ZFC does not make reference to inaccessibles but it's provable in ZFC + 1 inaccessible because you can construct a model of ZFC in the first inaccessible

[Mario Carneiro]

and ditto for each inaccessible after that, it demonstrates the consistency of the theory with one less inaccessible

[Jason Rute]

Increases in consistency strength can be used to prove new theorems in the natural numbers. These theorems don’t have to mention explicitly anything about the objects used in the new axioms used to increase consistency strength.

[Fernando Chu]

right, thanks for clearing up my confusion (for those interested, I understood the theorem quoted in a wrong manner; the point there is that this new system "looks" and "feels" like using inaccessible cardinals but it really isn't doing that)

[Timothy Chow]

I hope it's not bad form to post to an old conversation that petered out a long time ago, but I have some comments to make that I think this community would find interesting and might not be fully aware of.

Avoiding universes and staying strictly within ZFC is something that some people care about. The number of such people is pretty small, I think, but it includes Peter Scholze. See this MathOverflow discussion: https://mathoverflow.net/q/382270/

As already discussed earlier in this conversation, universes are irrelevant to Fermat's Last Theorem, but there is another question that quite a few people seem to be interested in, which is whether FLT is provable in first-order Peano arithmetic (PA for short). I personally believe that many people who ask this question are making the mistake of conflating "Is FLT is provable in PA?" with "Does FLT have an elementary proof?" and they're asking the former question when they're really interested in the latter. Angus Macintyre's appendix to Chapter 1 ("The Impact of Gödel's Incompleteness Theorems on Mathematics") of Kurt Gödel and the Foundations of Mathematics: Horizons of Truth gives a pretty convincing heuristic argument that one can take the existing proof of FLT and replace all the fancy machinery (which makes liberal use of infinite sets) with "finitary approximations"; the result would be a PA-proof, but not a proof that most people would call "elementary." Regardless, as I said, some people do seem to be interested in whether FLT is provable in PA, and this is a nontrivial question.

More generally, "reverse mathematics" is a growing field, and aims to find the weakest possible axioms needed to prove a theorem. The usual framework for reverse mathematics is second-order arithmetic, in the sense of Steve Simpson's book Subsystems of Second-Order Arithmetic (SOSOA). The phrase "second-order arithmetic" is somewhat confusing, because it's really a two-sorted first-order system, but the terminology is too entrenched to change at this point in time.

I gather that Lean is not designed to answer these kinds of reverse-mathematical questions, and at least at the moment, the Lean community has much bigger fish to fry. But I think it's good to be aware that eliminating universes is not the only reverse-mathematical question that people are interested in.

Here's a related question. I have a vague and quite possibly incorrect impression that HOL Light is based on simple type theory and therefore equiconsistent with bounded Zermelo set theory. If so, then what are the prospects for semi-automatically translating portions of mathlib into HOL Light? Would doing so help us answer provability-in-ZFC questions?

[David Michael Roberts]

Antoine Chambert-Loir said:

Maybe this is implicit in the thread, but in his lectures at Collège de France, Thierry Coquand insisted that the basic Martin-Löf type theory, with universes, is weaker than second order Peano arithmetic.

Do you have a link to Coquand's lectures or write-ups of them?

[Rémy Degenne]

Videos of the lectures: https://www.college-de-france.fr/fr/enseignements/audios-videos?f%5B0%5D=chair%3A83777

[David Michael Roberts]

@Rémy Degenne thanks, but that's nine videos, in a language I know the bare basics of, if that. Which one should I look at?

[Rémy Degenne]

I think I saw the passage Antoine is referring to, so it is probably in one of the first three videos. I can't be more precise than that.

[David Michael Roberts]

Thanks!

[Mario Carneiro]

David Michael Roberts said:

Antoine Chambert-Loir said:

Maybe this is implicit in the thread, but in his lectures at Collège de France, Thierry Coquand insisted that the basic Martin-Löf type theory, with universes, is weaker than second order Peano arithmetic.

Do you have a link to Coquand's lectures or write-ups of them?

I recently had cause to track down the sources for this claim (that MLTT embeds in second order arithmetic). I found the following:

1. https://www2.math.uu.se/~palmgren/universe.pdf
2. https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.44
3. https://www.sciencedirect.com/science/article/pii/S0049237X08713648
4. https://link.springer.com/chapter/10.1007/978-3-319-63334-3_14
5. https://www.researchgate.net/publication/247365747_Recursive_models_for_constructive_set_theories

I believe (3) is the original reference, (4) is an overview of related results, and (5) was the easiest for me to understand the full construction

[James E Hanson]

Timothy Chow said:

Here's a related question. I have a vague and quite possibly incorrect impression that HOL Light is based on simple type theory and therefore equiconsistent with bounded Zermelo set theory. If so, then what are the prospects for semi-automatically translating portions of mathlib into HOL Light? Would doing so help us answer provability-in-ZFC questions?

Mario and I had a conversation a while ago about the prospects of (semi-)automatically removing universes from Lean proofs. My best attempt at this would be something like the following procedure (inspired by a technique occasionally used in model theory to 'fake' the existence of inaccessible cardinals): Suppose we're trying to prove something about some objects that naturally live in $H_{\kappa}$ (the set of sets hereditarily of cardinality $\kappa$) for some cardinal $\kappa$. By passing to a forcing extension (or maybe to an inner model like $L[H_\kappa]$), we can ensure that for all $n < \omega$, $\kappa^{+n} = \beth_n(\kappa)$ (i.e., GCH holds in an interval above $\kappa$) without changing the truth value of statements of quantifiers bounded by elements of $H_{\kappa}$. Now the sets $U_n \coloneqq H_{\kappa^{+n}}$ behave approximately like Grothendieck universes in that (for $n > 0$) they're closed under the formation of $W$-types and satisfy that for any $A \in U_n$ and $B : A \to U_m$, $\prod_{x \in A} B(x) \in U_{\max\{n+1,m\}}$ (as opposed to an actual sequence of Grothendieck universes, which would satisfy $\prod_{x \in A} B(x) \in U_{\max\{n,m\}}$). Note that you do actually need to do something like passing to a forcing extension to ensure that this happens: If $2^\kappa = \kappa^{++}$ for all cardinals $\kappa$ but there are no inaccessible cardinals, then there is no sequence of cardinals with this property.

Now I'm not that hopeful about this working in practice, but in principle one might be able to inspect some of the proofs in mathlib and determine that these weaker closure properties are actually sufficient, thereby showing that the proofs can be converted into ZFC proofs.

[Timothy Chow]

Interesting; I hadn't heard of your proposal before. The main proposal I'm aware of for semi-automatically eliminating universes is Feferman's, as described for example in Shulman's paper, Set theory for category theory (he calls the system ZFC/S). What advantages do you think your proposal has over Feferman's?

[Jason Rute]

I’ve also seen this proposal for what seems to me to be a very manual and tedious process of rebuilding math inside ZFC inside Lean. https://members.loria.fr/SMerz/stages/2025-zfc-lean.html. (The two proposers are not on this Zulip. :sad:)

[James E Hanson]

Timothy Chow said:

Interesting; I hadn't heard of your proposal before. The main proposal I'm aware of for semi-automatically eliminating universes is Feferman's, as described for example in Shulman's paper, Set theory for category theory (he calls the system ZFC/S). What advantages do you think your proposal has over Feferman's?

One issue I anticipate with Feferman universes is that their inaccessible-like properties are only metatheoretical. In particular, if $V_\kappa$ and $V_\mu$ are Feferman universes with $\kappa < \mu$, then in general $V_\kappa$ won't look special internally inside $V_\mu$. For instance, $\kappa$ may be singular.

From the point of view of type theory, this means that Feferman universes are closed under things like 'small products of first-order definable families of small sets,' which seem to be hard to formalize cleanly in type-theoretic language.

[Mario Carneiro]

Jason Rute said:

I’ve also seen this proposal for what seems to me to be a very manual and tedious process of rebuilding math inside ZFC inside Lean. https://members.loria.fr/SMerz/stages/2025-zfc-lean.html. (The two proposers are not on this Zulip. :sad:)

A less manual and tedious way to get lots of math in ZFC in Lean is using the translation from metamath