zlacker

At least in Isabelle/ML, it seems like in practice there are also untrusted "oracles" that a proof can invoke to generate "thm" objects [0], and it's not entirely trivial to automatically ensure that only trusted sources are used in a project [1], unless I am misunderstanding the linked thread.

Of course there's no free lunch, as you say, in making sure that high-level proofs are lowered into the trusted part correctly, but it's certainly a piece that should ideally be as simple as possible.

[0] https://lists.cam.ac.uk/sympa/arc/cl-isabelle-users/2025-02/...

[1] https://lists.cam.ac.uk/sympa/arc/cl-isabelle-users/2025-02/...