Comment by josh-wrale

Maybe there will be an OpenAPI or gRPC of proofs to solve this to some extent, or maybe lean4 is already that, ig.