一句话定义：可信内核（Trusted Kernel）是形式化证明系统里那个必须无条件相信的最小程序，它只干一件事——检查一份完整证明是否真的成立。如果一个系统做到"所有自动化最终都产出一个能被这个小程序独立检查的证明对象"，就说它满足 De Bruijn 准则（De Bruijn criterion）。
为什么必须这么设计
以 Lean 为例。借助 Curry-Howard 对应，写证明等于写一个类型恰好是该命题的程序项，也就是证明项（proof term）。但写证明的过程极其复杂：归纳、化简、调自动化策略（tactic）、搜引理，任何一环出 bug 都可能"证"出假命题。
于是设计上做了一次切割：所有花哨的部分只负责生成候选证明项，生成完就退场；真正拍板的只有内核，它做类型检查（type checking）——这个证明项的类型，的的确确就是所要证的那个命题吗？是就通过，不是就报错。
打个比方，内核像一个只认基本算式的计算器。你可以用任何高级软件、任何 AI 助手去猜答案，但最终必须把推理翻译成它能验算的最基础步骤；它算不通，前面说得再漂亮都不算数。
和相邻概念的区别
内核不等于整个证明助手。编辑器、补全、策略库出问题，只会让你写不出来，不会让你证错。内核也不管公理（axiom）：它只保证"从公理到结论"的推导合法，公理本身是否可接受不在它管辖范围。
| 层次 | 典型内容 | 必须信任？ |
|---|---|---|
| 界面与工具链 | 编辑器、补全、诊断 | 否 |
| 自动化与模型 | 策略、搜索、AI 生成的草稿 | 否 |
| 可信内核 | 证明项校验 | 是 |
| 逻辑前提 | 选择公理、外延性等 | 是（但它不是程序） |
对从业者的实际意义
这解释了"AI 做数学"的信任链条：模型输出只是候选草稿，真正背书的是内核。但也别把它神化——sorry、额外引入的 axiom、unsafe 代码、绕开内核的判定捷径，都能开出天窗。审阅一份形式化结果时该问：结论依赖了哪些公理？有没有未闭合的占位？由哪个内核检查？
信任基（Trusted Computing Base, TCB）该多大，是工程取舍。内核通常只有几千行量级，小到可以人工审计；整个系统则是几十万行，没人能逐行看完。把信任压缩到最小，就是 De Bruijn 准则的全部意义。各系统的具体实现与版本差异，以官方文档为准。