The consistency of NF in Lean?

[Timothy Y. Chow]

On Sun, 27 Feb 2022, JOSEPH SHIPMAN wrote:
> Remind me, what’s the consistency strength that was claimed?

Long ago, Specker showed that NF is equiconsistent with (Russellian 
unramified) typed set theory plus the axiom schema of typical ambiguity.

https://en.wikipedia.org/wiki/New_Foundations#The_consistency_problem_and_related_partial_results

Assuming Holmes's argument is correct, it constructs a model of TST + 
Ambiguity in ZFA.  (ZFA is used for convenience since the heart of the 
proof is a Fraenkel-Mostowski construction; you can use ZF if you prefer.) 
>From what I've heard, his proof can probably be carried out in something 
weaker, but since the community hasn't yet digested even the ZFA proof, 
working too hard on weakening the metatheory seems premature...

Tim