Pretty much. The kernel of a proof assistant is the absolutely trusted core, and ultimately gets to decide what is or isn't a proven mathematical fact (so rough

Pretty much. The kernel of a proof assistant is the absolutely trusted core, and ultimately gets to decide what is or isn't a proven mathematical fact (so roughly a kernel resource). Over that, you build a huge amount of (userspace) tooling that doesn't have to be absolutely trusted since its job is just to talk into the kernel and get theorems. A kernel bug manifests as the kernel deciding that something is a theorem which shouldn't be. The worst case is when it decides that False is a theorem, from which it immediately follows that absolutely everything is a theorem. The HOL Light kernel (mentioned in the article) is about 500 lines from one file (https://github.com/jrh13/hol-light/blob/master/fusion.ml https://github.com/jrh13/hol-light/blob/master/fusion.ml), and is a very straightforward implementation of a simple type theory (https://en.wikipedia.org/wiki/HOL_Light#Logical_foundations https://en.wikipedia.org/wiki/HOL_Light#Logical_foundations). I'm not so familiar with Lean, but it would appear its kernel is spread over this C++ directory: https://github.com/leanprover/lean4/tree/master/src/kernel https://github.com/leanprover/lean4/tree/master/src/kernel. As mentioned in the article, HOL Light gets away with a lot because it only cares about delivering theorems. Other systems want to retain the proofs as artifacts (sometimes called certificates), and once you do that, you need to make sure these artifacts aren't stupidly huge or otherwise useless. Provers such as Rocq (and I assume Lean) additionally want their proof objects to contain decent executable algorithms backing the proof. HOL Light also does pretty much no evaluation. The most it understands of evaluation is that (λx. f) x = f. If you want to evaluate anything more complex than this, you build that in "userspace" and you do all the equational reasoning manually via the kernel. Lean and Rocq kernels do full evaluation of recursive functions, so they have to come installed with an API for building those recursive functions and internal checking to make sure those functions are terminating. The article's author is asking whether you could redo something like Lean and Rocq where the recursive function API was much simpler. I've wondered for a while whether you could also have the evaluator as basic as HOL Light's, and do the rest in userspace. I think there were theorem provers like this that went out of fashion decades ago. It used to be a much more exciting space before Lean somehow got everyone's attention. The author is the co-creator of Isabelle/HOL, and is still not sure why there is so much more excitement for Lean than for simple type theory.