I thought so too. I understand the TLA+ part but Lean not as much.