Oracle for assessing proposition validity within env

Stream: lean4

[Simone Melchiorre Chiarello]

Hi all.
This is my first exercise in Lean4 after lingering a lot, so please forgive my lack of expertise.
I am trying to set up an oracle which takes as input an expression, and returns whether the expression is valid in a given environment. In short, my requirements are the following:

• An API exposed (say REST but doesn't really matter)
• Accepting as input a data structure containing an expression, say the proof of 1 = 1.
• An "environment" consisting of a subset of imports of Mathlib or directly from Lean4 core or custom.
• A method to parse the input and typecheck it with the environment. For example, I'd assume that a small environment with just Nat and the definition of rfl would be enough for 1 = 1.
• It returns either "true" or "false" depending on whether the expression typechecks or not (i.e. it's a valid proof).
• Various utility endpoints like the set of definitions and theorems of the environment or similar.

My question is whether something similar exists already, and if not, how to start implementing it. The most important part in my project is to really strip down Mathlib and only use subsets of it for a particular oracle, the rest of the features are just for UX so not really important.

Here is a badly formed, mostly broken, ChatGPT-assisted code which works for a sample input.
https://github.com/lsqrl/LeanOraclePoC
This one in particular has the entire Mathlib in the dependencies (and doesn't work for most of inputs), however my goal would be to remove that and just add a subset of it. Feel free to ignore if you find it not suitable for the scope.