descriptive claim
Although Lean has many bugs, trusting Lean's results requires trusting only its kernel.
Unresolved speaker · Mathematics Just Changed Forever — Kevin Hartnett · 26 Oct 2026
In their words
The transcript segments this claim was taken from
“We have the notion of a small trusted kernel. Uh, Lean's massive, has zillions of bugs, right? But to trust our results, uh, in Lean, you only need to trust the kernel.”14:00Report a misattribution
0.95how strongly it was put, not whether it is true
0.90importance to the conversation
0.98confidence the claim was read correctly