I am Director of CSLib (Computer Science Library in Lean) at Renaissance Philanthropy, a global open-source initiative funded by Amazon and Google building a formal library of computer science in Lean. I am also a participant in DARPA's ExpMath programme on AI-assisted mathematical formalization.