Back

Two additional thoughts:

1. It is remarkable how much "decoupling" is achieved by the Lean+Blueprint combo. Contributors can work locally on proving a lemma, without necessarily fully understanding the global proof structure. Mathematicians who do understand the global proof can work on the blueprint, without necessarily understanding the mechanics of Lean. Lean experts can work on technical aspects of the implementation, such as optimizing the selection of classes and definitions, without needing expert domain knowledge. A theorem can be formalized, before, after, or concurrently with the lemmas it relies on, or the applications it has. Two participants who want to discuss some finer point of the argument can localize to a very specific and highly formalized step and have a constructive discussion even if they come from quite different backgrounds. It allows for (certain types of) high-level mathematical activity to be done at a far more atomized level than is usually possible.

2. I have still not fully exploited the potential of Github Copilot. One trick I am beginning to learn: once one has written down one line of code, present (as a comment in Mathematical English) a description of a similar line of code, and often Copilot will correctly adapt the previous line to give the right syntax. Here I include two such examples: having formalized a quantity $I_1$, Copilot makes it easy to formalize a similar quantity $I_2$; and having stated an estimate for the former, it can also formalize an estimate for the latter.