[impodimium]

Interesting that this only specialized for Lean4 and not for similar like Coq

[DoctorOetker]

I would have preferred actual proof objects, as in Metamath's: separate the actual proof from the heuristics used to find it (also valuable, but a different thing).