@placholdr @scathach
not sure how you mean. it's a funclang to be used as an interactive proof assistant for implementing maths rigorously, so findings can be computer-verified. maybe there's some syntactic similarity? haven't used here lean before yet, so can't comment much more on except there's been some adoption from "real mathematicians" compared to other systems, which is kind of exciting