## Stream: maths

### Topic: digits

#### Kevin Buzzard (Feb 02 2019 at 09:52):

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 (Feb 02 2019 at 09:54):

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 (Feb 02 2019 at 10:07):

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

#### Mario Carneiro (Feb 02 2019 at 10:08):

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

#### Mario Carneiro (Feb 02 2019 at 10:10):

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

#### Kevin Buzzard (Feb 02 2019 at 10:33):

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 (Feb 02 2019 at 10:35):

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 (Feb 02 2019 at 10:36):

It was nat subtraction hell

#### Kevin Buzzard (Feb 02 2019 at 10:37):

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

#### Mario Carneiro (Feb 02 2019 at 10:42):

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 (Feb 02 2019 at 10:44):

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 (Feb 02 2019 at 14:29):

For nats, isn't there to_digits?

#### Kevin Buzzard (Feb 02 2019 at 14:31):

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

Oh, no it's not!

#### Kevin Buzzard (Feb 02 2019 at 14:31):

the reversal takes place in repr.

Last updated: May 12 2021 at 08:14 UTC