I agree! Martín Escardó never tires to say that he uses the Agda proof assistant in exactly this sense, as a kind of interactive blackboard for taking notes and structuring his thoughts. The vast TypeTopology repository is the result of years of following this philosophy: https://github.com/martinescardo/TypeTopology

The Curry-Howard correspondence.

For instance, in mathematics, we have A ⇒ A (every statement implies itself, for instance "if it rains, then it rains"); and analogously, in programming, we have the identity function of type A → A (which reads a value as input and outputs the same value).

This is the tip of an enormous iceberg identifying, in a certain precise sense, proving with programming (and stating mathematical assertions with specifying the desired behavior of a program).

However, programming is a bit more general than proving: Circular proofs are simply of no value, whereas looping programs can still be valuable. For instance, I for sure hope that the main loop of the browser I'm currently using to fill out this textbox does not prematurely stop.

>we have the identity function of type A → A (which reads a value as input and outputs the same value)

That only exists in theoretical computer science. In real computer programming, you always have some bounds to the value of A.

I think it is time to repost Against Curry-Howard Mysticism (https://liamoc.net/forest/loc-000S/index.xml)

Strongly depends on the subbubble of mathematics. In some parts of type theory / formal proofs for instance, there is a rather strong rejection of LLMs (for moral reasons in addition to quality reasons). The proof assistant Agda was even forked for this reason: https://types.pl/@amy/116522250630340534

> Of course Lean proofs are rarely a good way to understand proofs, but hopefully they can be used to generate more human understandable arguments.

I would object to the first part: Of course there is a nontrivial learning curve, but then I'd argue that non-slop Lean/Agda/Rocq/... formalizations are amazing for understanding proofs. A good formalization presents the outline and the key arguments in nicely structured form, and then, unlike pen-and-paper proofs, also allow you to get the details on every single step, exactly to your desired level of depth.

The proofs in Martín Escardó's TypeTopology Agda repository come immediately to my mind as an example. [An interactive Agda tutorial is here: lets-play-agda.quasicoherent.io]

In contrast, LLM-generated formalizations can currently be extremely messy. They certify truth and can also contain interesting arguments, but substantial work is required to bring them into a shape that contributes to the actual goal of improving our understanding of the mathematical landscape.