Algebra is generous

Still feeling uninspired so I'm just going to keep going with the Dutilh Novaes book. I never did read the last chapter, 'Debiasing', so let's see what I can find there. Nice quote from d'Alembert:

Algebra is generous; she often gives more than is asked of her.

Dutilh Novaes's argument here seems to be that this happens because reasoning inside a desemantified (is that a word?) formal language means inhibiting your usual biases:

Our strong tendency towards seeking confirmation for the beliefs we already hold - our doxastic conservativeness - stands in the way of the discovery of truly novel (unknown, unexpected) facts about a given phenomenon.

Hmm. This seems off to me, though I should definitely consider it more. Mainly seems off because most types of desemantified (I'm just going to make it a word) formula-shuffling you can do don't lead anywhere very interesting, and you normally have to rely on some form of domain knowledge to guide your formula-shuffling towards something worthwhile. Otherwise computers would be finding more interesting new mathematical results than they are right now.

Though maybe there's a weaker version of this that I do believe? Like sometimes your intuitions do pull in a completely wrong direction (c.f. the bat and ball) and turning off your associations with the target domain and just formula-shuffling works a lot better. My sense is that this is sometimes the story for why 'algebra is generous', but not what's normally going on. Idk.

Even if I'm not convinced yet, there's some nice stuff next about how the desemantification works. Basically, you instead focus on sensorimotor manipulation of the symbols themselves - transforming squiggles on the page according to certain internalised rules. While you're doing that, you can just think about squiggle transformation and not the domain it's supposed to map to.

Because the latter resorts to cognitive systems and processes that are quite different from those involved in our spontaneous tendency to rely on prior belief, the likelihood of the fundamental bias cropping in again is probably much lower.

OK, so on the next page Dutilh Novaes gets to my computer argument from earlier:

... there is still an important amount of creativity and insight involved in producing a non-trivial proof, often pertaining to, for example, clever renaming of schematic letter, unexpected instantiations of axioms, etc. Indeed, even automated theorem-provers must contain some heuristic features in the program, as 'brute force' alone (i.e., mere combinatorial procedures) leads to an explosion of trivial, uninformative theorems.

Still, the formalism does succeed at blocking some of the intuitive-but-wrong answers, 'and this is sufficient for the debiasing effect to occur'.

Right, that's about a pomodoro's worth of writing about this book, that'll do for now.