The paper tackles a foundational question in mathematical logic: how much set theory can you prove is consistent using a particular style of formal type theory, without assuming certain powerful "choice" axioms? The standard way of interpreting set theory inside type theory (treating sets as tree-like structures) is known to validate most of Zermelo-Fraenkel set theory (ZF), but a key piece called the Replacement axiom seemed to require a special operator that converts relational descriptions into functions. Without that operator, experts expected the system to be substantially weaker than full ZF. The paper shows this expectation was wrong.
The authors work inside Lean's type theory, assuming only the law of excluded middle (every statement is either true or false) and nothing else, no choice, no quotients, no extensionality. They prove that ZF is consistent, meaning they construct a model of it. The technical engine is a feature of dependent type theory called "large elimination of the accessibility predicate," which lets you do recursion over well-founded trees even when the trees can be as large as the entire universe of sets. This recursion is subtle because later steps depend on the results of earlier ones, and propositions guard which branches are taken. Using this, they can compute any ordinal that is specified by a well-founded description, without ever having to pick a single preferred map, by instead taking all definable maps simultaneously.
The argument splits into two cases. Either at some point a cumulative hierarchy level already forms a model of ZF (in which case you are done), or the recursion succeeds in making the tree-structured sets satisfy the Replacement axiom for all propositional relations, again giving a model of ZF. Either way, ZF has a model and is therefore consistent. As a bonus, the authors show the argument works even with just the double negation of excluded middle, a weaker assumption, and they connect this to the double negation of Markov's principle, tying the result into broader questions about constructive logic. The proof is fully formalized in Lean.