I don't know why you're getting downvoted because I think this is an interesting idea.

Completely impossible but still interesting and fun to explore.

But you don't need the power of Lean to do something like this. I would recommend starting with something like Prolog or RDF triples