# Zulip Chat Archive

## 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...

#### Chris Hughes (Feb 19 2019 at 00:02):

Why shouldn't your daughter be forced to learn about cosines?

#### Kevin Buzzard (Feb 19 2019 at 07:45):

Because she doesn't like maths

Last updated: May 11 2021 at 16:22 UTC