## Stream: maths

### Topic: real number game

#### Kevin Buzzard (Mar 26 2020 at 11:41):

People ask me about other games like natural number game, and I've suggested several in the past, but the one which seems to get the most attention is the real number game. Gavin Thomson, a student of David Corfield in Kent, was coming up to London to work with me on it for four months, arriving in May. Of course this is all now very much up in the air. But @Daniel Keys has also expressed an interest. I will try and get David onto Zulip and we'll see if we can coordinate something here. There is already a public repo but we are nowhere near a release.

My experience in writing these games is that for each concept you either import it from Lean (if you just want to use it) or write it from scratch. If you write it from scratch you want one file with all the definitions and the coercions and the notation and a basic API for mathematicians all in term mode, and tell the mathematician not to open it. And then you need a file full of theorems, some of which are sorried and where you can supply tactic mode proofs with steps which feel like about the same pace as a book might go if they were explaining the argument carefully. Sometimes this is a challenge to do in Lean, with "basic" maths steps which seem to be tough for beginners to formalise. Is more API needed in this case?

One thing I wanted to have in the natural number game was more than one sorry to fill in on a page, possibly with the later sorry depending on the first one. I sometimes felt this was a hindrance in NNG.

Does anyone have any comments on issues they had with the natural number game which we could perhaps avoid in the real number game? I am really hoping to be able to cut down on the number of words used in the tactic descriptions, or at least get them out of the way somehow so you can see the key definition at the top of my waffle, and the key lemma in the middle of it, whilst still being able to code in a small box at the bottom.

#### Jiekai (Mar 26 2020 at 11:48):

NNG meaning?

#### Mario Carneiro (Mar 26 2020 at 11:49):

natural number game

#### Daniel Keys (Mar 26 2020 at 17:19):

Doing things from scratch like in the NNG has the advantage of possibly being able to show the players more details. But working with Cauchy sequences or Dedekind cuts does seem quite a bit more far-fetched than Peano's axioms.
Using mathlib's capabilities in data.real.basic etc. might hide some foundational stuff but is naturally amenable to teaching the tools built by the community, which is also desirable.
Could a middle way be better in this case? For example, importing at each level (or as needed) in the game a file that imports, in turn, only the needed tools. Say import from bounds.lean just is_lub and a few other related items when working on results related to the supremum, then list them in the theorems on the left.

#### Gavin Thomson (Mar 26 2020 at 20:14):

Following! thanks for the invite Kevin :)
So I still want to help but I won't be up to speed for a few weeks at least. :( So I may be a bit clueless until then. I also should admit that I don't have any experience of working with real numbers in lean yet.

I think the question of how much is built from scratch and how much is imported maybe depends on who the RNG is aimed at?

I can only speak for my own experience of undergrad analysis, but I think we saw axioms for the reals first and then proceeded along the lines mentioned on the RNG page -- sups and infs, sequences and limits, series.

I thought the NNG was good for anyone who wanted a first taste of interactive theorem proving, undergrad or professional. But I guess seeing how to build an explicit construction from scratch would be more useful for professionals than students?
I see Kevin was looking at similar questions ages ago: https://leanprover-community.github.io/archive/116395maths/43084bounds.html

I agree that a second game could use less text -- my feeling was that the NNG had to give some motivation for tactics that might seem weird without any knowledge of the nuts and bolts of type theory, term rewriting etc. But I think anyone playing RNG should have played NNG.

#### Kevin Buzzard (Apr 08 2020 at 13:52):

How much will I have to hack lean 3 or mathlib to get things like (1,3] : set real to work? Lean's conventions for intervals are nowhere near what a mathematician is used to.

#### Patrick Massot (Apr 08 2020 at 13:53):

I use [a, b] : set real in my lectures, without hacking anything.

Oh nice

#### Patrick Massot (Apr 08 2020 at 13:53):

I didn't try with (1, 3] (which is a stupid notation anyway).

#### Kevin Buzzard (Apr 08 2020 at 13:54):

I'd be happy with ]1, 3]

#### Kevin Buzzard (Apr 08 2020 at 13:54):

Can you give me a link to some code or something?

#### Patrick Massot (Apr 08 2020 at 13:55):

notation ]a, b] := Ioc a b
#check ]1, 3]


#### Kevin Buzzard (Apr 08 2020 at 13:55):

And this is ok in practice?

noooo

#### Kevin Buzzard (Apr 08 2020 at 13:55):

I promise I'll never use lists

Same here.

Or tuples

or commas

#### Patrick Massot (Apr 08 2020 at 13:56):

And I had no trouble at all using [a, b] to mean [a, b].

#### Kevin Buzzard (Apr 08 2020 at 13:56):

Yeah we don't use commas either

#### Patrick Massot (Apr 08 2020 at 13:56):

What's wrong with you software people?

#### Mario Carneiro (Apr 08 2020 at 13:56):

I will remind you that one place lists come up is in tactics

Hmm

#### Patrick Massot (Apr 08 2020 at 13:57):

That will be the ultimate parser test for @Sebastian Ullrich: can we use this notation in Lean 4 without destroying Lean?

#### Mario Carneiro (Apr 08 2020 at 13:57):

how dare us use ascii

#### Mario Carneiro (Apr 08 2020 at 13:58):

I'm pretty sure that this notation is ambiguous

#### Kevin Buzzard (Apr 08 2020 at 13:58):

Not if you have a sane unifier

#### Kevin Buzzard (Apr 08 2020 at 13:58):

Remember lists don't exist in maths departments

#### Kevin Buzzard (Apr 08 2020 at 13:59):

The notation for a list is $x_1, x_2, \ldots$

#### Kevin Buzzard (Apr 08 2020 at 13:59):

Who needs brackets

#### Mario Carneiro (Apr 08 2020 at 14:00):

well, you don't have to nest that expression in anything except for english text

#### Mario Carneiro (Apr 08 2020 at 14:00):

it's not so easy in a theorem prover

#### Reid Barton (Apr 08 2020 at 14:01):

We already use various forms of absolute value/norm which seem to work all right

#### Reid Barton (Apr 08 2020 at 14:02):

If you want all of [a, b], [a, b[, ]a, b[, ]a, b] to work that adds another twist though

#### Sebastian Ullrich (Apr 08 2020 at 14:03):

Yeah, that's a no. When you declare a notation/parser starting with ], Lean 4 will not accept [a, b] anymore.

#### Kevin Buzzard (Apr 08 2020 at 14:03):

And the English versions too

When is Lean 5?

#### Reid Barton (Apr 08 2020 at 15:20):

Mario how long have you been waiting to use :maple_leaf:

Last updated: May 14 2021 at 18:28 UTC