This sounds very interesting and relevant to the goals of the CSLib initiative that apparently just got started. I don't have a better public link to it now except this LinkedIn post (perhaps there's a Zulip tag):

https://www.linkedin.com/posts/lean-fro_leanlang-cslib-forma...