I like the Lean formalizations — I hadn't thought seriously of asking for that before but might try it with some stuff I've been working on.