## Stream: maths

### Topic: Teaching with Lean

#### Kevin Buzzard (Feb 13 2019 at 15:10):

Patrick's formatter has made me start thinking about not teaching Lean to students, but teaching maths to students using the formatter. In fact I am even considering a situation where Lean code is hidden completely and the students can only see the tactic state, which is far less intimidating.

This made me realise the importance of notation. A student can understand Hn : n <= N but something like ha : is_limit a l is far harder for a mathematician to read. Is there unicode notation for $\lim_{n\to\infty}$ somehow?

#### Kevin Buzzard (Feb 13 2019 at 15:11):

@Patrick Massot could we even have something which processes the tactic state and turns is_limit a l into a LaTeX $\lim_{n\to\infty}a_n=\ell$?

#### Reid Barton (Feb 13 2019 at 15:14):

You may be able to approximate this somewhat with notation, possibly?

#### Wojciech Nawrocki (Feb 13 2019 at 15:18):

You can definitely do something like

constants (a l: Foo)
notation lim n->∞ a = l := is_limit a l
#check is_limit a l -- lim n->∞ a = l : Foo


alhough I don't know how well the equality notation will play with notation for eq. Maybe Lean 4's extensible parsers could make this better.

#### Kevin Buzzard (Feb 13 2019 at 15:19):

I am motivated to make it look as sexy as possible. Can I make the n -> infty as a subscript using unicode?

#### Reid Barton (Feb 13 2019 at 15:20):

Hmm, but this assumes the free variable is named n

#### Reid Barton (Feb 13 2019 at 15:20):

but I guess the original is_limit a l didn't even have an explicit free variable anywhere, so I don't know what to do about that

#### Wojciech Nawrocki (Feb 13 2019 at 15:23):

AFAIK Unicode only provides a predefined set of subscript characters and neither an arrow nor the infty sign seem to be among them.

#### Patrick Massot (Feb 13 2019 at 16:41):

Yes, unicode won't be good enough. But mathjax is good enough. However it will have to be a regex-based hack (until we get a Lean 4 structured tactic state).

#### Patrick Massot (Feb 13 2019 at 16:42):

My tool could filter the tactic state before displaying it and search and replace there

#### Kevin Buzzard (Feb 18 2019 at 22:28):

https://xenaproject.wordpress.com/2019/02/18/224/ -- me trying to tell kids aged 14-15 about inductive types ;-) It went OK! I think that next time I might try 15-16 though...