digits

Stream: maths

[Kevin Buzzard]

The students at Imperial do random maths in Lean. I run a puzzle-solving club where we look at recreational questions involving things such as digit sums of integers. In my 1st year exam last year there is a question about decimal expansions, where we needed to know for example that $71/100$ had no 8's in its decimal expansion. As far as I know there is no way of getting the $$n$$th decimal digit of a natural, or the $$n$$th digit after the decimal point of a real number, in mathlib. I need this stuff now (for example to formalise the questions and solutions on last year's M1F paper). Is this sort of nonsense the sort of thing which should go into mathlib or should I just make my own little library? I don't mind either way, it just occurs to me that whilst I am clear in my opinions that most undergraduate level pure maths is a very natural target for mathlib (indeed I think that the more undergraduate level pure maths is in mathlib, the more pure mathematicians will take Lean seriously), I am less clear about this fringe stuff. It's easy to write (indeed I've written it) but I now don't quite know what to do with it.

[Patrick Massot]

I would say we want mathlib to be ready to formalize such questions, but we don't want the questions and their answers

[Mario Carneiro]

A function nat -> list (fin b) giving the base-b expansion of a nat seems like a good idea for mathlib

[Mario Carneiro]

probably you want the digits to come out in reverse order though

[Mario Carneiro]

I would avoid fixation on base 10 though, for most of the functions and especially the theory

[Kevin Buzzard]

I did develop a general base b theory but lots of results needed b>=2 so in the end I got bored and switched to 10.

[Kevin Buzzard]

On the other hand I never needed induction on b :-) so maybe I should have persevered. Proving things like "all the digits of b^N - 1 are b-1" was horrible but this was perhaps part of the recreation, not the library part

[Kevin Buzzard]

It was nat subtraction hell

[Kevin Buzzard]

Yes, reverse order was far easier to work with in practice. I wanted results about things like sum of last digits

[Mario Carneiro]

I agree that b >= 2 is a natural restriction in this context (although there is a useful thing to do for b = 1 as well)

[Mario Carneiro]

for b^N - 1 I would try to rewrite it as k + k*b+... +k*b^(N-1) where b = k+1

[Bryan Gin-ge Chen]

For nats, isn't there to_digits?

[Kevin Buzzard]

For repr yes, but that's the wrong way round :-)

[Kevin Buzzard]

Oh, no it's not!

[Kevin Buzzard]

the reversal takes place in repr.