A proof assistant turns a mathematical argument into something a computer can check completely. The proof is written in a formal language, and the kernel, a small program, verifies that each step follows from the last. If the kernel accepts it, the conclusion follows from the stated assumptions.
Two limits matter for anyone relying on one. The kernel is software and can have bugs: in July 2026 a flaw in Lean’s kernel let a false “disproof” of the Collatz conjecture pass, and it was fixed within hours. And the check only covers whether the conclusion follows from the statement as written. Someone still has to confirm the statement says what was meant.