programmatically (ab)use lean4

Stream: lean4

[Huỳnh Trần Khanh]

is there a way to use lean4 as a library? like I want to write an external program that interfaces with Lean 4 and produces Lean 4 proofs

[Huỳnh Trần Khanh]

and because Lean 4 is complex and I couldn't identify a usable restricted subset string concatenation is unlikely to be feasible and an API would be really helpful

[Marc Huisinga]

https://github.com/leanprover/lean4/blob/master/src/Lean/Elab/Frontend.lean#L97
The language server interacts with Lean 4 in a similar way