The top answer is currently two points ahead. As suggested in the comments, I'll rename the room from "Proof Assistants" to "Tautology" unless anyone objects.

@ammkrn I'm more interested about making the de Bruijn criterion rigorous. Even 1500 lines of code seems quite big to satisfy the de Bruijn criterion.

Every proof assistant claims to satisfy the de Bruijn criterion and have a "small kernel", even Coq(!). I'd have a hard time accepting the claims for Coq, and for Lean. BUT that's not "the end of the world". There are valid reasons to want a large kernel.

@ammkrn Do you have any references for extracting Lean proofs and checking them in metamath zero? That's an intriguing approach to things.

@AlexNelson Yeah, fair enough. There seems to be some fuzziness about whether "the de Bruijn criterion" means that your tool produces terms in a kernel language or whether it actually means the thing can be verified by hand. Lean satisfies the first one, so I would guess that's what the developers are claiming when they say it.

The metamath zero thing is about using a Lean kernel to output proof steps that correspond to the mm0 formalization of Lean's type theory, which is in the repo's examples folder. I modified a fork of the kernel to do it as a text file while the checking is going on, but I think mm0's developer is super busy, then Lean 4 happened, and I wrote an mm0 verifier and learned a bunch about that, so the plan is to redo it at some point so that it directly outputs mm0 terms instead of a text file.

@ammkrn I honestly have no idea how anyone could honestly interpret the de Bruijn criterion to mean the first condition, because almost anything satisfies that condition. I mean, we have the definition of the de Bruijn criterion, I can't see how "A Mathematical Assistant satisfying the possibility of independent checking by a small program" ...could be interpreted as "produces terms in a kernel language".

@AlexNelson "Proof assistants satisfy the "de Bruijn criterion" when they produce proof terms in small kernel languages, even when they use complicated and extensible procedures to seek out proofs in the first place. " adam.chlipala.net/cpdt/html/Intro.html

Send him an email and ask, I guess.

@ammkrn Yeah, Adam Chlipala is using an idiosyncratic (very non-standard) meaning of the term. Everything satisfies the de Bruijn criterion, if we take him seriously...which means it's a bad definition.

Or you're emphasizing the wrong parts, as he continues in the next sentence, "To believe a proof, we can ignore the possibility of bugs during search and just rely on a (relatively small) proof-checking kernel that we apply to the result of the search."

I don't think he could have given a more direct explanation of what he thinks the definition is, so it's definitely not the second option.

With all due respect, it sounds like you are intentionally trying to read your own opinion into what he has written. It's clear he's speaking about a small kernel with a complicated search procedure outside the kernel. The difference between the definition I supplied and his is that he requires proof objects to be produced, whereas the definition I supplied does not.

In fact, he goes on to explain ACL2 fails to satisfy the de Bruijn criterion because it doesn't produce a proof object.

(True to form, he argues Coq is "small"...everyone who uses Coq insists this, for reasons which elude me...)

"ACL2 fails to satisfy the de Bruijn criterion because it doesn't produce a proof object." Not, "ACL2 fails to satisfy the de Bruijn criterion beacuse its kernel isn't small." Please also notice that he does not say "coq is small", he says "Coq meets the de Bruijn criterion".

If I write a proof assistant with a 100k loc kernel that can also export proofs in a simple kernel language which can be verified by a totally external 300 loc verifier, does my proof assistant satisfy your definition of the de Bruijn criterion?

@wizzwizz4 We have a little more than 600 users and the question has a little more than 200 views, so only a third of the people have seen this question; and there's a banner on the main site encouraging people to visit the meta.

Also the difference between the suggestions has been greater than 2 or 3 to 1 (physics.meta.stackexchange.com/q/1028/170832 or space.meta.stackexchange.com/q/2/20766) in some cases.

Wait, or change in a month or two; waiting for a bigger pool of voters is more inclusive; as was noted in your comment on the question.

@GuyCoder "...I have no problem with the information being in both. My view is that the tag wiki should be more than just a simple few lines and links, let them stand on their own with enough information but not so much that it takes more than ~three minutes of reading." I agree with what you are saying, but I simply think it is better to include the info in both answer and tag wiki rather than just tag wiki.

Can those with edit approval check the review queue. There are some import tag edits ready for a second approval.