We will discuss some lessons learned from the PNT+ Project (complex analysis, large collaborative formalization, interactions with AI systems), and the Real Analysis Game (pedagogical aspects, technical aspects).