(As an aside, back in the late 1970s I started writing papers that involved formulas generated by computer. And in one particular paper, the formulas happened to have lots of occurrences of the number 9. But the experienced typist who typed the paper — yes, from a manuscript — replaced every “9” with a “g”. When I asked her why, she said, “Well, there are never explicit 9’s in papers!”)