Rado Kirov has been one of several people working through the exercises in my Lean formalization of my Analysis I textbook at https://github.com/teorth/analysis . For several months he proceeded by hand, teaching himself Lean; see https://rkirov.github.io/posts/lean3/ and https://rkirov.github.io/posts/lean4/ . But recently, he switched to using Claude Code, significantly accelerating the process, to the point where all the exercises in three section could be formalized in a weekend, with only a few hours of active intervention: https://rkirov.github.io/posts/lean5/ . This is already notable, but I found Rado's description of his precise workflow, and the carefully curated prompt at https://github.com/rkirov/analysis/blob/main/CLAUDE.md he used, to be particularly interesting, with an emphasis not on just solving the exercises, but aligning it to his desired writing style, and identifying "pitfalls" in the formalizing process (which were recorded separately at https://github.com/rkirov/analysis/blob/main/TACTICS.md ). These sorts of experiments suggest that using these automated tools to take over tedious tasks such as formalization may not necessarily reduce our own capability to achieve these tasks; with the proper workflows, they could actually enhance our understanding of the process.