I only skimmed the content, but I like the bit at the beginning talking about how proof verification can change mathematical style.

I want to highlight the linked paper: https://arxiv.org/pdf/2405.04699.

I wonder if the ability we have in forester to expand/collapse sections, link to things, and rearrange material could also have a similar stylistic result, without any computation-outsourced. That is, even if you are doing proofs fully manually, you could have one version of your paper where you laid out those proofs, and another version in which you simply granularly referred to the first version.

1 Like